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