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

Theorem fmptco 5271
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 4761 . 2 Rel (𝐺𝐹)
2 funmpt 4879 . . 3 Fun (x A𝑇)
3 funrel 4860 . . 3 (Fun (x A𝑇) → Rel (x A𝑇))
42, 3ax-mp 7 . 2 Rel (x A𝑇)
5 fmptco.1 . . . . . . . . . . . . 13 ((φ x A) → 𝑅 B)
6 eqid 2037 . . . . . . . . . . . . 13 (x A𝑅) = (x A𝑅)
75, 6fmptd 5263 . . . . . . . . . . . 12 (φ → (x A𝑅):AB)
8 fmptco.2 . . . . . . . . . . . . 13 (φ𝐹 = (x A𝑅))
98feq1d 4975 . . . . . . . . . . . 12 (φ → (𝐹:AB ↔ (x A𝑅):AB))
107, 9mpbird 156 . . . . . . . . . . 11 (φ𝐹:AB)
11 ffun 4989 . . . . . . . . . . 11 (𝐹:AB → Fun 𝐹)
1210, 11syl 14 . . . . . . . . . 10 (φ → Fun 𝐹)
13 funbrfv 5153 . . . . . . . . . . 11 (Fun 𝐹 → (z𝐹u → (𝐹z) = u))
1413imp 115 . . . . . . . . . 10 ((Fun 𝐹 z𝐹u) → (𝐹z) = u)
1512, 14sylan 267 . . . . . . . . 9 ((φ z𝐹u) → (𝐹z) = u)
1615eqcomd 2042 . . . . . . . 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 1703 . . . 4 (φ → (u(z𝐹u u𝐺w) ↔ u(u = (𝐹z) (z𝐹u u𝐺w))))
21 exsimpl 1505 . . . . . . 7 (u(u = (𝐹z) (z𝐹u u𝐺w)) → u u = (𝐹z))
22 isset 2555 . . . . . . 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 4991 . . . . . . . . . . 11 (𝐹:AB → dom 𝐹 = A)
2710, 26syl 14 . . . . . . . . . 10 (φ → dom 𝐹 = A)
2827eleq2d 2104 . . . . . . . . 9 (φ → (z dom 𝐹z A))
2928biimpar 281 . . . . . . . 8 ((φ z A) → z dom 𝐹)
30 funfvex 5133 . . . . . . . 8 ((Fun 𝐹 z dom 𝐹) → (𝐹z) V)
3125, 29, 30syl2anc 391 . . . . . . 7 ((φ z A) → (𝐹z) V)
3231adantrr 448 . . . . . 6 ((φ (z A w = z / x𝑇)) → (𝐹z) V)
3332ex 108 . . . . 5 (φ → ((z A w = z / x𝑇) → (𝐹z) V))
34 breq2 3758 . . . . . . . . 9 (u = (𝐹z) → (z𝐹uz𝐹(𝐹z)))
35 breq1 3757 . . . . . . . . 9 (u = (𝐹z) → (u𝐺w ↔ (𝐹z)𝐺w))
3634, 35anbi12d 442 . . . . . . . 8 (u = (𝐹z) → ((z𝐹u u𝐺w) ↔ (z𝐹(𝐹z) (𝐹z)𝐺w)))
3736ceqsexgv 2667 . . . . . . 7 ((𝐹z) V → (u(u = (𝐹z) (z𝐹u u𝐺w)) ↔ (z𝐹(𝐹z) (𝐹z)𝐺w)))
38 funfvbrb 5221 . . . . . . . . . . 11 (Fun 𝐹 → (z dom 𝐹z𝐹(𝐹z)))
3912, 38syl 14 . . . . . . . . . 10 (φ → (z dom 𝐹z𝐹(𝐹z)))
4039, 28bitr3d 179 . . . . . . . . 9 (φ → (z𝐹(𝐹z) ↔ z A))
418fveq1d 5121 . . . . . . . . . 10 (φ → (𝐹z) = ((x A𝑅)‘z))
42 fmptco.3 . . . . . . . . . 10 (φ𝐺 = (y B𝑆))
43 eqidd 2038 . . . . . . . . . 10 (φw = w)
4441, 42, 43breq123d 3768 . . . . . . . . 9 (φ → ((𝐹z)𝐺w ↔ ((x A𝑅)‘z)(y B𝑆)w))
4540, 44anbi12d 442 . . . . . . . 8 (φ → ((z𝐹(𝐹z) (𝐹z)𝐺w) ↔ (z A ((x A𝑅)‘z)(y B𝑆)w)))
46 nfcv 2175 . . . . . . . . . . 11 xz
47 nfv 1418 . . . . . . . . . . . 12 xφ
48 nffvmpt1 5127 . . . . . . . . . . . . . 14 x((x A𝑅)‘z)
49 nfcv 2175 . . . . . . . . . . . . . 14 x(y B𝑆)
50 nfcv 2175 . . . . . . . . . . . . . 14 xw
5148, 49, 50nfbr 3798 . . . . . . . . . . . . 13 x((x A𝑅)‘z)(y B𝑆)w
52 nfcsb1v 2876 . . . . . . . . . . . . . 14 xz / x𝑇
5352nfeq2 2186 . . . . . . . . . . . . 13 x w = z / x𝑇
5451, 53nfbi 1478 . . . . . . . . . . . 12 x(((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇)
5547, 54nfim 1461 . . . . . . . . . . 11 x(φ → (((x A𝑅)‘z)(y B𝑆)ww = z / x𝑇))
56 fveq2 5119 . . . . . . . . . . . . . 14 (x = z → ((x A𝑅)‘x) = ((x A𝑅)‘z))
5756breq1d 3764 . . . . . . . . . . . . 13 (x = z → (((x A𝑅)‘x)(y B𝑆)w ↔ ((x A𝑅)‘z)(y B𝑆)w))
58 csbeq1a 2854 . . . . . . . . . . . . . 14 (x = z𝑇 = z / x𝑇)
5958eqeq2d 2048 . . . . . . . . . . . . 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 2554 . . . . . . . . . . . . . 14 w V
63 simpl 102 . . . . . . . . . . . . . . . . 17 ((y = 𝑅 u = w) → y = 𝑅)
6463eleq1d 2103 . . . . . . . . . . . . . . . 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 2051 . . . . . . . . . . . . . . . 16 ((y = 𝑅 u = w) → (u = 𝑆w = 𝑇))
6964, 68anbi12d 442 . . . . . . . . . . . . . . 15 ((y = 𝑅 u = w) → ((y B u = 𝑆) ↔ (𝑅 B w = 𝑇)))
70 df-mpt 3810 . . . . . . . . . . . . . . 15 (y B𝑆) = {⟨y, u⟩ ∣ (y B u = 𝑆)}
7169, 70brabga 3991 . . . . . . . . . . . . . 14 ((𝑅 B w V) → (𝑅(y B𝑆)w ↔ (𝑅 B w = 𝑇)))
725, 62, 71sylancl 392 . . . . . . . . . . . . 13 ((φ x A) → (𝑅(y B𝑆)w ↔ (𝑅 B w = 𝑇)))
73 simpr 103 . . . . . . . . . . . . . . 15 ((φ x A) → x A)
746fvmpt2 5195 . . . . . . . . . . . . . . 15 ((x A 𝑅 B) → ((x A𝑅)‘x) = 𝑅)
7573, 5, 74syl2anc 391 . . . . . . . . . . . . . 14 ((φ x A) → ((x A𝑅)‘x) = 𝑅)
7675breq1d 3764 . . . . . . . . . . . . 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 2612 . . . . . . . . . 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 425 . . . . . . . 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 436 . . . . . 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 620 . . . 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 2554 . . . 4 z V
8988, 62opelco 4449 . . 3 (⟨z, w (𝐺𝐹) ↔ u(z𝐹u u𝐺w))
90 df-mpt 3810 . . . . 5 (x A𝑇) = {⟨x, v⟩ ∣ (x A v = 𝑇)}
9190eleq2i 2101 . . . 4 (⟨z, w (x A𝑇) ↔ ⟨z, w {⟨x, v⟩ ∣ (x A v = 𝑇)})
92 nfv 1418 . . . . . 6 x z A
9352nfeq2 2186 . . . . . 6 x v = z / x𝑇
9492, 93nfan 1454 . . . . 5 x(z A v = z / x𝑇)
95 nfv 1418 . . . . 5 v(z A w = z / x𝑇)
96 eleq1 2097 . . . . . 6 (x = z → (x Az A))
9758eqeq2d 2048 . . . . . 6 (x = z → (v = 𝑇v = z / x𝑇))
9896, 97anbi12d 442 . . . . 5 (x = z → ((x A v = 𝑇) ↔ (z A v = z / x𝑇)))
99 eqeq1 2043 . . . . . 6 (v = w → (v = z / x𝑇w = z / x𝑇))
10099anbi2d 437 . . . . 5 (v = w → ((z A v = z / x𝑇) ↔ (z A w = z / x𝑇)))
10194, 95, 88, 62, 98, 100opelopabf 4001 . . . 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 4378 1 (φ → (𝐺𝐹) = (x A𝑇))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1242  wex 1378   wcel 1390  Vcvv 2551  csb 2846  cop 3369   class class class wbr 3754  {copab 3807  cmpt 3808  dom cdm 4287  ccom 4291  Rel wrel 4292  Fun wfun 4838  wf 4840  cfv 4844
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3865  ax-pow 3917  ax-pr 3934
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3352  df-sn 3372  df-pr 3373  df-op 3375  df-uni 3571  df-br 3755  df-opab 3809  df-mpt 3810  df-id 4020  df-xp 4293  df-rel 4294  df-cnv 4295  df-co 4296  df-dm 4297  df-rn 4298  df-res 4299  df-ima 4300  df-iota 4809  df-fun 4846  df-fn 4847  df-f 4848  df-fv 4852
This theorem is referenced by:  fmptcof  5272  fcompt  5274  fcoconst  5275  ofco  5668
  Copyright terms: Public domain W3C validator