Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fmptco Structured version   GIF version

Theorem fmptco 5232
 Description: Composition of two functions expressed as ordered-pair class abstractions. If 𝐹 has the equation ( x + 2 ) and 𝐺 the equation ( 3 * z ) then (𝐺 ∘ 𝐹) has the equation ( 3 * ( x + 2 ) ) . (Contributed by FL, 21-Jun-2012.) (Revised by Mario Carneiro, 24-Jul-2014.)
Hypotheses
Ref Expression
fmptco.1 ((φ x A) → 𝑅 B)
fmptco.2 (φ𝐹 = (x A𝑅))
fmptco.3 (φ𝐺 = (y B𝑆))
fmptco.4 (y = 𝑅𝑆 = 𝑇)
Assertion
Ref Expression
fmptco (φ → (𝐺𝐹) = (x A𝑇))
Distinct variable groups:   x,A   x,y,B   y,𝑅   φ,x   x,𝑆   y,𝑇
Allowed substitution hints:   φ(y)   A(y)   𝑅(x)   𝑆(y)   𝑇(x)   𝐹(x,y)   𝐺(x,y)

Proof of Theorem fmptco
Dummy variables v u w z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 4723 . 2 Rel (𝐺𝐹)
2 funmpt 4841 . . 3 Fun (x A𝑇)
3 funrel 4822 . . 3 (Fun (x A𝑇) → Rel (x A𝑇))
42, 3ax-mp 7 . 2 Rel (x A𝑇)
5 fmptco.1 . . . . . . . . . . . . 13 ((φ x A) → 𝑅 B)
6 eqid 2023 . . . . . . . . . . . . 13 (x A𝑅) = (x A𝑅)
75, 6fmptd 5224 . . . . . . . . . . . 12 (φ → (x A𝑅):AB)
8 fmptco.2 . . . . . . . . . . . . 13 (φ𝐹 = (x A𝑅))
98feq1d 4937 . . . . . . . . . . . 12 (φ → (𝐹:AB ↔ (x A𝑅):AB))
107, 9mpbird 156 . . . . . . . . . . 11 (φ𝐹:AB)
11 ffun 4951 . . . . . . . . . . 11 (𝐹:AB → Fun 𝐹)
1210, 11syl 14 . . . . . . . . . 10 (φ → Fun 𝐹)
13 funbrfv 5114 . . . . . . . . . . 11 (Fun 𝐹 → (z𝐹u → (𝐹z) = u))
1413imp 115 . . . . . . . . . 10 ((Fun 𝐹 z𝐹u) → (𝐹z) = u)
1512, 14sylan 267 . . . . . . . . 9 ((φ z𝐹u) → (𝐹z) = u)
1615eqcomd 2028 . . . . . . . 8 ((φ z𝐹u) → u = (𝐹z))
1716a1d 22 . . . . . . 7 ((φ z𝐹u) → (u𝐺wu = (𝐹z)))
1817expimpd 345 . . . . . 6 (φ → ((z𝐹u u𝐺w) → u = (𝐹z)))
1918pm4.71rd 374 . . . . 5 (φ → ((z𝐹u u𝐺w) ↔ (u = (𝐹z) (z𝐹u u𝐺w))))
2019exbidv 1689 . . . 4 (φ → (u(z𝐹u u𝐺w) ↔ u(u = (𝐹z) (z𝐹u u𝐺w))))
21 exsimpl 1492 . . . . . . 7 (u(u = (𝐹z) (z𝐹u u𝐺w)) → u u = (𝐹z))
22 isset 2538 . . . . . . 7 ((𝐹z) V ↔ u u = (𝐹z))
2321, 22sylibr 137 . . . . . 6 (u(u = (𝐹z) (z𝐹u u𝐺w)) → (𝐹z) V)
2423a1i 9 . . . . 5 (φ → (u(u = (𝐹z) (z𝐹u u𝐺w)) → (𝐹z) V))
2512adantr 261 . . . . . . . 8 ((φ z A) → Fun 𝐹)
26 fdm 4953 . . . . . . . . . . 11 (𝐹:AB → dom 𝐹 = A)
2710, 26syl 14 . . . . . . . . . 10 (φ → dom 𝐹 = A)
2827eleq2d 2090 . . . . . . . . 9 (φ → (z dom 𝐹z A))
2928biimpar 281 . . . . . . . 8 ((φ z A) → z dom 𝐹)
30 funfvex 5094 . . . . . . . 8 ((Fun 𝐹 z dom 𝐹) → (𝐹z) V)
3125, 29, 30syl2anc 393 . . . . . . 7 ((φ z A) → (𝐹z) V)
3231adantrr 451 . . . . . 6 ((φ (z A w = z / x𝑇)) → (𝐹z) V)
3332ex 108 . . . . 5 (φ → ((z A w = z / x𝑇) → (𝐹z) V))
34 breq2 3721 . . . . . . . . 9 (u = (𝐹z) → (z𝐹uz𝐹(𝐹z)))
35 breq1 3720 . . . . . . . . 9 (u = (𝐹z) → (u𝐺w ↔ (𝐹z)𝐺w))
3634, 35anbi12d 445 . . . . . . . 8 (u = (𝐹z) → ((z𝐹u u𝐺w) ↔ (z𝐹(𝐹z) (𝐹z)𝐺w)))
3736ceqsexgv 2649 . . . . . . 7 ((𝐹z) V → (u(u = (𝐹z) (z𝐹u u𝐺w)) ↔ (z𝐹(𝐹z) (𝐹z)𝐺w)))
38 funfvbrb 5182 . . . . . . . . . . 11 (Fun 𝐹 → (z dom 𝐹z𝐹(𝐹z)))
3912, 38syl 14 . . . . . . . . . 10 (φ → (z dom 𝐹z𝐹(𝐹z)))
4039, 28bitr3d 179 . . . . . . . . 9 (φ → (z𝐹(𝐹z) ↔ z A))
418fveq1d 5082 . . . . . . . . . 10 (φ → (𝐹z) = ((x A𝑅)‘z))
42 fmptco.3 . . . . . . . . . 10 (φ𝐺 = (y B𝑆))
43 eqidd 2024 . . . . . . . . . 10 (φw = w)
4441, 42, 43breq123d 3731 . . . . . . . . 9 (φ → ((𝐹z)𝐺w ↔ ((x A𝑅)‘z)(y B𝑆)w))
4540, 44anbi12d 445 . . . . . . . 8 (φ → ((z𝐹(𝐹z) (𝐹z)𝐺w) ↔ (z A ((x A𝑅)‘z)(y B𝑆)w)))
46 nfcv 2161 . . . . . . . . . . 11 xz
47 nfv 1404 . . . . . . . . . . . 12 xφ
48 nffvmpt1 5088 . . . . . . . . . . . . . 14 x((x A𝑅)‘z)
49 nfcv 2161 . . . . . . . . . . . . . 14 x(y B𝑆)
50 nfcv 2161 . . . . . . . . . . . . . 14 xw
5148, 49, 50nfbr 3761 . . . . . . . . . . . . 13 x((x A𝑅)‘z)(y B𝑆)w
52 nfcsb1v 2859 . . . . . . . . . . . . . 14 xz / x𝑇
5352nfeq2 2172 . . . . . . . . . . . . 13 x w = z / x𝑇
5451, 53nfbi 1465 . . . . . . . . . . . 12 x(((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇)
5547, 54nfim 1448 . . . . . . . . . . 11 x(φ → (((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇))
56 fveq2 5080 . . . . . . . . . . . . . 14 (x = z → ((x A𝑅)‘x) = ((x A𝑅)‘z))
5756breq1d 3727 . . . . . . . . . . . . 13 (x = z → (((x A𝑅)‘x)(y B𝑆)w ↔ ((x A𝑅)‘z)(y B𝑆)w))
58 csbeq1a 2837 . . . . . . . . . . . . . 14 (x = z𝑇 = z / x𝑇)
5958eqeq2d 2034 . . . . . . . . . . . . 13 (x = z → (w = 𝑇w = z / x𝑇))
6057, 59bibi12d 224 . . . . . . . . . . . 12 (x = z → ((((x A𝑅)‘x)(y B𝑆)ww = 𝑇) ↔ (((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇)))
6160imbi2d 219 . . . . . . . . . . 11 (x = z → ((φ → (((x A𝑅)‘x)(y B𝑆)ww = 𝑇)) ↔ (φ → (((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇))))
62 vex 2537 . . . . . . . . . . . . . 14 w V
63 simpl 102 . . . . . . . . . . . . . . . . 17 ((y = 𝑅 u = w) → y = 𝑅)
6463eleq1d 2089 . . . . . . . . . . . . . . . 16 ((y = 𝑅 u = w) → (y B𝑅 B))
65 simpr 103 . . . . . . . . . . . . . . . . 17 ((y = 𝑅 u = w) → u = w)
66 fmptco.4 . . . . . . . . . . . . . . . . . 18 (y = 𝑅𝑆 = 𝑇)
6766adantr 261 . . . . . . . . . . . . . . . . 17 ((y = 𝑅 u = w) → 𝑆 = 𝑇)
6865, 67eqeq12d 2037 . . . . . . . . . . . . . . . 16 ((y = 𝑅 u = w) → (u = 𝑆w = 𝑇))
6964, 68anbi12d 445 . . . . . . . . . . . . . . 15 ((y = 𝑅 u = w) → ((y B u = 𝑆) ↔ (𝑅 B w = 𝑇)))
70 df-mpt 3773 . . . . . . . . . . . . . . 15 (y B𝑆) = {⟨y, u⟩ ∣ (y B u = 𝑆)}
7169, 70brabga 3955 . . . . . . . . . . . . . 14 ((𝑅 B w V) → (𝑅(y B𝑆)w ↔ (𝑅 B w = 𝑇)))
725, 62, 71sylancl 394 . . . . . . . . . . . . 13 ((φ x A) → (𝑅(y B𝑆)w ↔ (𝑅 B w = 𝑇)))
73 simpr 103 . . . . . . . . . . . . . . 15 ((φ x A) → x A)
746fvmpt2 5156 . . . . . . . . . . . . . . 15 ((x A 𝑅 B) → ((x A𝑅)‘x) = 𝑅)
7573, 5, 74syl2anc 393 . . . . . . . . . . . . . 14 ((φ x A) → ((x A𝑅)‘x) = 𝑅)
7675breq1d 3727 . . . . . . . . . . . . 13 ((φ x A) → (((x A𝑅)‘x)(y B𝑆)w𝑅(y B𝑆)w))
775biantrurd 289 . . . . . . . . . . . . 13 ((φ x A) → (w = 𝑇 ↔ (𝑅 B w = 𝑇)))
7872, 76, 773bitr4d 209 . . . . . . . . . . . 12 ((φ x A) → (((x A𝑅)‘x)(y B𝑆)ww = 𝑇))
7978expcom 109 . . . . . . . . . . 11 (x A → (φ → (((x A𝑅)‘x)(y B𝑆)ww = 𝑇)))
8046, 55, 61, 79vtoclgaf 2594 . . . . . . . . . 10 (z A → (φ → (((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇)))
8180impcom 116 . . . . . . . . 9 ((φ z A) → (((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇))
8281pm5.32da 428 . . . . . . . 8 (φ → ((z A ((x A𝑅)‘z)(y B𝑆)w) ↔ (z A w = z / x𝑇)))
8345, 82bitrd 177 . . . . . . 7 (φ → ((z𝐹(𝐹z) (𝐹z)𝐺w) ↔ (z A w = z / x𝑇)))
8437, 83sylan9bbr 439 . . . . . 6 ((φ (𝐹z) V) → (u(u = (𝐹z) (z𝐹u u𝐺w)) ↔ (z A w = z / x𝑇)))
8584ex 108 . . . . 5 (φ → ((𝐹z) V → (u(u = (𝐹z) (z𝐹u u𝐺w)) ↔ (z A w = z / x𝑇))))
8624, 33, 85pm5.21ndd 608 . . . 4 (φ → (u(u = (𝐹z) (z𝐹u u𝐺w)) ↔ (z A w = z / x𝑇)))
8720, 86bitrd 177 . . 3 (φ → (u(z𝐹u u𝐺w) ↔ (z A w = z / x𝑇)))
88 vex 2537 . . . 4 z V
8988, 62opelco 4410 . . 3 (⟨z, w (𝐺𝐹) ↔ u(z𝐹u u𝐺w))
90 df-mpt 3773 . . . . 5 (x A𝑇) = {⟨x, v⟩ ∣ (x A v = 𝑇)}
9190eleq2i 2087 . . . 4 (⟨z, w (x A𝑇) ↔ ⟨z, w {⟨x, v⟩ ∣ (x A v = 𝑇)})
92 nfv 1404 . . . . . 6 x z A
9352nfeq2 2172 . . . . . 6 x v = z / x𝑇
9492, 93nfan 1442 . . . . 5 x(z A v = z / x𝑇)
95 nfv 1404 . . . . 5 v(z A w = z / x𝑇)
96 eleq1 2083 . . . . . 6 (x = z → (x Az A))
9758eqeq2d 2034 . . . . . 6 (x = z → (v = 𝑇v = z / x𝑇))
9896, 97anbi12d 445 . . . . 5 (x = z → ((x A v = 𝑇) ↔ (z A v = z / x𝑇)))
99 eqeq1 2029 . . . . . 6 (v = w → (v = z / x𝑇w = z / x𝑇))
10099anbi2d 440 . . . . 5 (v = w → ((z A v = z / x𝑇) ↔ (z A w = z / x𝑇)))
10194, 95, 88, 62, 98, 100opelopabf 3965 . . . 4 (⟨z, w {⟨x, v⟩ ∣ (x A v = 𝑇)} ↔ (z A w = z / x𝑇))
10291, 101bitri 173 . . 3 (⟨z, w (x A𝑇) ↔ (z A w = z / x𝑇))
10387, 89, 1023bitr4g 212 . 2 (φ → (⟨z, w (𝐺𝐹) ↔ ⟨z, w (x A𝑇)))
1041, 4, 103eqrelrdv 4339 1 (φ → (𝐺𝐹) = (x A𝑇))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98  ∃wex 1362   = wceq 1374   ∈ wcel 1376  Vcvv 2534  ⦋csb 2829  ⟨cop 3331   class class class wbr 3717  {copab 3770   ∈ cmpt 3771  dom cdm 4248   ∘ ccom 4252  Rel wrel 4253  Fun wfun 4800  ⟶wf 4802  ‘cfv 4806 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-10 1379  ax-11 1380  ax-i12 1381  ax-bnd 1382  ax-4 1383  ax-14 1388  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-i5r 1412  ax-ext 2005  ax-sep 3828  ax-pow 3880  ax-pr 3897 This theorem depends on definitions:  df-bi 110  df-3an 878  df-tru 1232  df-nf 1330  df-sb 1629  df-eu 1885  df-mo 1886  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-ral 2288  df-rex 2289  df-rab 2292  df-v 2536  df-sbc 2741  df-csb 2830  df-un 2901  df-in 2903  df-ss 2910  df-pw 3314  df-sn 3334  df-pr 3335  df-op 3337  df-uni 3534  df-br 3718  df-opab 3772  df-mpt 3773  df-id 3984  df-xp 4254  df-rel 4255  df-cnv 4256  df-co 4257  df-dm 4258  df-rn 4259  df-res 4260  df-ima 4261  df-iota 4771  df-fun 4808  df-fn 4809  df-f 4810  df-fv 4814 This theorem is referenced by:  fmptcof  5233  fcompt  5235  fcoconst  5236  ofco  5628
 Copyright terms: Public domain W3C validator