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

Theorem tfrexlem 5870
Description: The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
Hypotheses
Ref Expression
tfrexlem.1 A = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}
tfrexlem.2 (φx(Fun 𝐹 (𝐹x) V))
Assertion
Ref Expression
tfrexlem ((φ 𝐶 𝑉) → (recs(𝐹)‘𝐶) V)
Distinct variable groups:   x,f,y,A   f,𝐹,x,y
Allowed substitution hints:   φ(x,y,f)   𝐶(x,y,f)   𝑉(x,y,f)

Proof of Theorem tfrexlem
Dummy variables 𝑒 g u v 𝑡 w z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5103 . . . . 5 (z = 𝐶 → (recs(𝐹)‘z) = (recs(𝐹)‘𝐶))
21eleq1d 2088 . . . 4 (z = 𝐶 → ((recs(𝐹)‘z) V ↔ (recs(𝐹)‘𝐶) V))
32imbi2d 219 . . 3 (z = 𝐶 → ((φ → (recs(𝐹)‘z) V) ↔ (φ → (recs(𝐹)‘𝐶) V)))
4 inss2 3135 . . . . . . 7 (suc suc z ∩ On) ⊆ On
5 ssorduni 4163 . . . . . . 7 ((suc suc z ∩ On) ⊆ On → Ord (suc suc z ∩ On))
64, 5ax-mp 7 . . . . . 6 Ord (suc suc z ∩ On)
7 vex 2538 . . . . . . . . . 10 z V
87sucex 4175 . . . . . . . . 9 suc z V
98sucex 4175 . . . . . . . 8 suc suc z V
109inex1 3865 . . . . . . 7 (suc suc z ∩ On) V
1110uniex 4124 . . . . . 6 (suc suc z ∩ On) V
12 elon2 4062 . . . . . 6 ( (suc suc z ∩ On) On ↔ (Ord (suc suc z ∩ On) (suc suc z ∩ On) V))
136, 11, 12mpbir2an 837 . . . . 5 (suc suc z ∩ On) On
14 tfrexlem.1 . . . . . . 7 A = {fx On (f Fn x y x (fy) = (𝐹‘(fy)))}
1514tfrlem3 5848 . . . . . 6 A = {vz On (v Fn z u z (vu) = (𝐹‘(vu)))}
16 tfrexlem.2 . . . . . . 7 (φx(Fun 𝐹 (𝐹x) V))
17 fveq2 5103 . . . . . . . . . 10 (x = z → (𝐹x) = (𝐹z))
1817eleq1d 2088 . . . . . . . . 9 (x = z → ((𝐹x) V ↔ (𝐹z) V))
1918anbi2d 440 . . . . . . . 8 (x = z → ((Fun 𝐹 (𝐹x) V) ↔ (Fun 𝐹 (𝐹z) V)))
2019cbvalv 1776 . . . . . . 7 (x(Fun 𝐹 (𝐹x) V) ↔ z(Fun 𝐹 (𝐹z) V))
2116, 20sylib 127 . . . . . 6 (φz(Fun 𝐹 (𝐹z) V))
2215, 21tfrlemi1 5867 . . . . 5 ((φ (suc suc z ∩ On) On) → g(g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))))
2313, 22mpan2 403 . . . 4 (φg(g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))))
2415recsfval 5853 . . . . . . . . . . 11 recs(𝐹) = A
2524breqi 3744 . . . . . . . . . 10 (zrecs(𝐹)yz Ay)
26 df-br 3739 . . . . . . . . . 10 (z Ay ↔ ⟨z, y A)
27 eluni 3557 . . . . . . . . . 10 (⟨z, y A(⟨z, y A))
2825, 26, 273bitri 195 . . . . . . . . 9 (zrecs(𝐹)y(⟨z, y A))
297sucid 4103 . . . . . . . . . . . . . . . . 17 z suc z
30 simpr 103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((⟨z, y A) → A)
31 vex 2538 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 V
3214, 31tfrlem3a 5847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ( A𝑡 On ( Fn 𝑡 𝑒 𝑡 (𝑒) = (𝐹‘(𝑒))))
3330, 32sylib 127 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨z, y A) → 𝑡 On ( Fn 𝑡 𝑒 𝑡 (𝑒) = (𝐹‘(𝑒))))
34 simprl 471 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨z, y A) (𝑡 On ( Fn 𝑡 𝑒 𝑡 (𝑒) = (𝐹‘(𝑒))))) → 𝑡 On)
35 simprrl 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⟨z, y A) (𝑡 On ( Fn 𝑡 𝑒 𝑡 (𝑒) = (𝐹‘(𝑒))))) → Fn 𝑡)
36 simpll 469 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((⟨z, y A) (𝑡 On ( Fn 𝑡 𝑒 𝑡 (𝑒) = (𝐹‘(𝑒))))) → ⟨z, y )
37 fnop 4928 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (( Fn 𝑡 z, y ) → z 𝑡)
3835, 36, 37syl2anc 393 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((⟨z, y A) (𝑡 On ( Fn 𝑡 𝑒 𝑡 (𝑒) = (𝐹‘(𝑒))))) → z 𝑡)
39 onelon 4070 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑡 On z 𝑡) → z On)
4034, 38, 39syl2anc 393 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((⟨z, y A) (𝑡 On ( Fn 𝑡 𝑒 𝑡 (𝑒) = (𝐹‘(𝑒))))) → z On)
4133, 40rexlimddv 2415 . . . . . . . . . . . . . . . . . . . . . . . 24 ((⟨z, y A) → z On)
4241adantl 262 . . . . . . . . . . . . . . . . . . . . . . 23 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → z On)
43 suceloni 4177 . . . . . . . . . . . . . . . . . . . . . . 23 (z On → suc z On)
4442, 43syl 14 . . . . . . . . . . . . . . . . . . . . . 22 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → suc z On)
45 suceloni 4177 . . . . . . . . . . . . . . . . . . . . . 22 (suc z On → suc suc z On)
4644, 45syl 14 . . . . . . . . . . . . . . . . . . . . 21 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → suc suc z On)
47 onss 4169 . . . . . . . . . . . . . . . . . . . . 21 (suc suc z On → suc suc z ⊆ On)
4846, 47syl 14 . . . . . . . . . . . . . . . . . . . 20 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → suc suc z ⊆ On)
49 df-ss 2908 . . . . . . . . . . . . . . . . . . . 20 (suc suc z ⊆ On ↔ (suc suc z ∩ On) = suc suc z)
5048, 49sylib 127 . . . . . . . . . . . . . . . . . . 19 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → (suc suc z ∩ On) = suc suc z)
5150unieqd 3565 . . . . . . . . . . . . . . . . . 18 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → (suc suc z ∩ On) = suc suc z)
52 eloni 4061 . . . . . . . . . . . . . . . . . . . 20 (suc z On → Ord suc z)
53 ordtr 4064 . . . . . . . . . . . . . . . . . . . 20 (Ord suc z → Tr suc z)
5444, 52, 533syl 17 . . . . . . . . . . . . . . . . . . 19 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → Tr suc z)
558unisuc 4099 . . . . . . . . . . . . . . . . . . 19 (Tr suc z suc suc z = suc z)
5654, 55sylib 127 . . . . . . . . . . . . . . . . . 18 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → suc suc z = suc z)
5751, 56eqtrd 2054 . . . . . . . . . . . . . . . . 17 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → (suc suc z ∩ On) = suc z)
5829, 57syl5eleqr 2109 . . . . . . . . . . . . . . . 16 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → z (suc suc z ∩ On))
59 fndm 4924 . . . . . . . . . . . . . . . . 17 (g Fn (suc suc z ∩ On) → dom g = (suc suc z ∩ On))
6059ad2antrr 460 . . . . . . . . . . . . . . . 16 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → dom g = (suc suc z ∩ On))
6158, 60eleqtrrd 2099 . . . . . . . . . . . . . . 15 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → z dom g)
627eldm 4459 . . . . . . . . . . . . . . 15 (z dom gx zgx)
6361, 62sylib 127 . . . . . . . . . . . . . 14 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → x zgx)
64 simpr 103 . . . . . . . . . . . . . . 15 ((((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) zgx) → zgx)
65 fneq2 4914 . . . . . . . . . . . . . . . . . . . . 21 (v = (suc suc z ∩ On) → (g Fn vg Fn (suc suc z ∩ On)))
66 raleq 2483 . . . . . . . . . . . . . . . . . . . . 21 (v = (suc suc z ∩ On) → (w v (gw) = (𝐹‘(gw)) ↔ w (suc suc z ∩ On)(gw) = (𝐹‘(gw))))
6765, 66anbi12d 445 . . . . . . . . . . . . . . . . . . . 20 (v = (suc suc z ∩ On) → ((g Fn v w v (gw) = (𝐹‘(gw))) ↔ (g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw)))))
6867rspcev 2633 . . . . . . . . . . . . . . . . . . 19 (( (suc suc z ∩ On) On (g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw)))) → v On (g Fn v w v (gw) = (𝐹‘(gw))))
6913, 68mpan 402 . . . . . . . . . . . . . . . . . 18 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → v On (g Fn v w v (gw) = (𝐹‘(gw))))
70 vex 2538 . . . . . . . . . . . . . . . . . . 19 g V
7114, 70tfrlem3a 5847 . . . . . . . . . . . . . . . . . 18 (g Av On (g Fn v w v (gw) = (𝐹‘(gw))))
7269, 71sylibr 137 . . . . . . . . . . . . . . . . 17 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → g A)
7372ad2antrr 460 . . . . . . . . . . . . . . . 16 ((((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) zgx) → g A)
74 simplrr 476 . . . . . . . . . . . . . . . 16 ((((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) zgx) → A)
75 simplrl 475 . . . . . . . . . . . . . . . . 17 ((((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) zgx) → ⟨z, y )
76 df-br 3739 . . . . . . . . . . . . . . . . 17 (zy ↔ ⟨z, y )
7775, 76sylibr 137 . . . . . . . . . . . . . . . 16 ((((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) zgx) → zy)
7815tfrlem5 5852 . . . . . . . . . . . . . . . . 17 ((g A A) → ((zgx zy) → x = y))
7978imp 115 . . . . . . . . . . . . . . . 16 (((g A A) (zgx zy)) → x = y)
8073, 74, 64, 77, 79syl22anc 1122 . . . . . . . . . . . . . . 15 ((((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) zgx) → x = y)
8164, 80breqtrd 3762 . . . . . . . . . . . . . 14 ((((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) zgx) → zgy)
8263, 81exlimddv 1760 . . . . . . . . . . . . 13 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → zgy)
83 vex 2538 . . . . . . . . . . . . . 14 y V
847, 83brelrn 4494 . . . . . . . . . . . . 13 (zgyy ran g)
8582, 84syl 14 . . . . . . . . . . . 12 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → y ran g)
86 elssuni 3582 . . . . . . . . . . . 12 (y ran gy ran g)
8785, 86syl 14 . . . . . . . . . . 11 (((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) (⟨z, y A)) → y ran g)
8887ex 108 . . . . . . . . . 10 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → ((⟨z, y A) → y ran g))
8988exlimdv 1682 . . . . . . . . 9 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → ((⟨z, y A) → y ran g))
9028, 89syl5bi 141 . . . . . . . 8 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → (zrecs(𝐹)yy ran g))
9190alrimiv 1736 . . . . . . 7 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → y(zrecs(𝐹)yy ran g))
92 fvss 5114 . . . . . . 7 (y(zrecs(𝐹)yy ran g) → (recs(𝐹)‘z) ⊆ ran g)
9391, 92syl 14 . . . . . 6 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → (recs(𝐹)‘z) ⊆ ran g)
9470rnex 4526 . . . . . . . 8 ran g V
9594uniex 4124 . . . . . . 7 ran g V
9695ssex 3868 . . . . . 6 ((recs(𝐹)‘z) ⊆ ran g → (recs(𝐹)‘z) V)
9793, 96syl 14 . . . . 5 ((g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → (recs(𝐹)‘z) V)
9897exlimiv 1471 . . . 4 (g(g Fn (suc suc z ∩ On) w (suc suc z ∩ On)(gw) = (𝐹‘(gw))) → (recs(𝐹)‘z) V)
9923, 98syl 14 . . 3 (φ → (recs(𝐹)‘z) V)
1003, 99vtoclg 2590 . 2 (𝐶 𝑉 → (φ → (recs(𝐹)‘𝐶) V))
101100impcom 116 1 ((φ 𝐶 𝑉) → (recs(𝐹)‘𝐶) V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wal 1226   = wceq 1228  wex 1362   wcel 1374  {cab 2008  wral 2284  wrex 2285  Vcvv 2535  cin 2893  wss 2894  cop 3353   cuni 3554   class class class wbr 3738  Tr wtr 3828  Ord word 4048  Oncon0 4049  suc csuc 4051  dom cdm 4272  ran crn 4273  cres 4274  Fun wfun 4823   Fn wfn 4824  cfv 4829  recscrecs 5841
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-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-13 1385  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-coll 3846  ax-sep 3849  ax-pow 3901  ax-pr 3918  ax-un 4120  ax-setind 4204
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2289  df-rex 2290  df-reu 2291  df-rab 2293  df-v 2537  df-sbc 2742  df-csb 2830  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-uni 3555  df-iun 3633  df-br 3739  df-opab 3793  df-mpt 3794  df-tr 3829  df-id 4004  df-iord 4052  df-on 4054  df-suc 4057  df-xp 4278  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-rn 4283  df-res 4284  df-ima 4285  df-iota 4794  df-fun 4831  df-fn 4832  df-f 4833  df-f1 4834  df-fo 4835  df-f1o 4836  df-fv 4837  df-recs 5842
This theorem is referenced by:  tfrex  5876
  Copyright terms: Public domain W3C validator