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

Theorem tfri3 5840
Description: Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 5838). Finally, we show that 𝐹 is unique. We do this by showing that any class B with the same properties of 𝐹 that we showed in parts 1 and 2 is identical to 𝐹. (Contributed by Jim Kingdon, 4-May-2019.)
Hypotheses
Ref Expression
tfri3.1 𝐹 = recs(𝐺)
tfri3.2 (Fun 𝐺 (𝐺x) V)
Assertion
Ref Expression
tfri3 ((B Fn On x On (Bx) = (𝐺‘(Bx))) → B = 𝐹)
Distinct variable groups:   x,B   x,𝐹   x,𝐺

Proof of Theorem tfri3
Dummy variable y is distinct from all other variables.
StepHypRef Expression
1 nfv 1403 . . . 4 x B Fn On
2 nfra1 2331 . . . 4 xx On (Bx) = (𝐺‘(Bx))
31, 2nfan 1441 . . 3 x(B Fn On x On (Bx) = (𝐺‘(Bx)))
4 nfv 1403 . . . . . 6 x(By) = (𝐹y)
53, 4nfim 1447 . . . . 5 x((B Fn On x On (Bx) = (𝐺‘(Bx))) → (By) = (𝐹y))
6 fveq2 5070 . . . . . . 7 (x = y → (Bx) = (By))
7 fveq2 5070 . . . . . . 7 (x = y → (𝐹x) = (𝐹y))
86, 7eqeq12d 2036 . . . . . 6 (x = y → ((Bx) = (𝐹x) ↔ (By) = (𝐹y)))
98imbi2d 219 . . . . 5 (x = y → (((B Fn On x On (Bx) = (𝐺‘(Bx))) → (Bx) = (𝐹x)) ↔ ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (By) = (𝐹y))))
10 r19.21v 2372 . . . . . 6 (y x ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (By) = (𝐹y)) ↔ ((B Fn On x On (Bx) = (𝐺‘(Bx))) → y x (By) = (𝐹y)))
11 rsp 2345 . . . . . . . . . 10 (x On (Bx) = (𝐺‘(Bx)) → (x On → (Bx) = (𝐺‘(Bx))))
12 onss 4142 . . . . . . . . . . . . . . . . . . 19 (x On → x ⊆ On)
13 tfri3.1 . . . . . . . . . . . . . . . . . . . . . 22 𝐹 = recs(𝐺)
14 tfri3.2 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐺 (𝐺x) V)
1513, 14tfri1 5838 . . . . . . . . . . . . . . . . . . . . 21 𝐹 Fn On
16 fvreseq 5163 . . . . . . . . . . . . . . . . . . . . 21 (((B Fn On 𝐹 Fn On) x ⊆ On) → ((Bx) = (𝐹x) ↔ y x (By) = (𝐹y)))
1715, 16mpanl2 413 . . . . . . . . . . . . . . . . . . . 20 ((B Fn On x ⊆ On) → ((Bx) = (𝐹x) ↔ y x (By) = (𝐹y)))
18 fveq2 5070 . . . . . . . . . . . . . . . . . . . 20 ((Bx) = (𝐹x) → (𝐺‘(Bx)) = (𝐺‘(𝐹x)))
1917, 18syl6bir 153 . . . . . . . . . . . . . . . . . . 19 ((B Fn On x ⊆ On) → (y x (By) = (𝐹y) → (𝐺‘(Bx)) = (𝐺‘(𝐹x))))
2012, 19sylan2 270 . . . . . . . . . . . . . . . . . 18 ((B Fn On x On) → (y x (By) = (𝐹y) → (𝐺‘(Bx)) = (𝐺‘(𝐹x))))
2120ancoms 255 . . . . . . . . . . . . . . . . 17 ((x On B Fn On) → (y x (By) = (𝐹y) → (𝐺‘(Bx)) = (𝐺‘(𝐹x))))
2221imp 115 . . . . . . . . . . . . . . . 16 (((x On B Fn On) y x (By) = (𝐹y)) → (𝐺‘(Bx)) = (𝐺‘(𝐹x)))
2322adantr 261 . . . . . . . . . . . . . . 15 ((((x On B Fn On) y x (By) = (𝐹y)) ((x On → (Bx) = (𝐺‘(Bx))) x On)) → (𝐺‘(Bx)) = (𝐺‘(𝐹x)))
2413, 14tfri2 5839 . . . . . . . . . . . . . . . . . . . 20 (x On → (𝐹x) = (𝐺‘(𝐹x)))
2524jctr 298 . . . . . . . . . . . . . . . . . . 19 ((x On → (Bx) = (𝐺‘(Bx))) → ((x On → (Bx) = (𝐺‘(Bx))) (x On → (𝐹x) = (𝐺‘(𝐹x)))))
26 jcab 522 . . . . . . . . . . . . . . . . . . 19 ((x On → ((Bx) = (𝐺‘(Bx)) (𝐹x) = (𝐺‘(𝐹x)))) ↔ ((x On → (Bx) = (𝐺‘(Bx))) (x On → (𝐹x) = (𝐺‘(𝐹x)))))
2725, 26sylibr 137 . . . . . . . . . . . . . . . . . 18 ((x On → (Bx) = (𝐺‘(Bx))) → (x On → ((Bx) = (𝐺‘(Bx)) (𝐹x) = (𝐺‘(𝐹x)))))
28 eqeq12 2034 . . . . . . . . . . . . . . . . . 18 (((Bx) = (𝐺‘(Bx)) (𝐹x) = (𝐺‘(𝐹x))) → ((Bx) = (𝐹x) ↔ (𝐺‘(Bx)) = (𝐺‘(𝐹x))))
2927, 28syl6 29 . . . . . . . . . . . . . . . . 17 ((x On → (Bx) = (𝐺‘(Bx))) → (x On → ((Bx) = (𝐹x) ↔ (𝐺‘(Bx)) = (𝐺‘(𝐹x)))))
3029imp 115 . . . . . . . . . . . . . . . 16 (((x On → (Bx) = (𝐺‘(Bx))) x On) → ((Bx) = (𝐹x) ↔ (𝐺‘(Bx)) = (𝐺‘(𝐹x))))
3130adantl 262 . . . . . . . . . . . . . . 15 ((((x On B Fn On) y x (By) = (𝐹y)) ((x On → (Bx) = (𝐺‘(Bx))) x On)) → ((Bx) = (𝐹x) ↔ (𝐺‘(Bx)) = (𝐺‘(𝐹x))))
3223, 31mpbird 156 . . . . . . . . . . . . . 14 ((((x On B Fn On) y x (By) = (𝐹y)) ((x On → (Bx) = (𝐺‘(Bx))) x On)) → (Bx) = (𝐹x))
3332exp43 354 . . . . . . . . . . . . 13 ((x On B Fn On) → (y x (By) = (𝐹y) → ((x On → (Bx) = (𝐺‘(Bx))) → (x On → (Bx) = (𝐹x)))))
3433com4t 79 . . . . . . . . . . . 12 ((x On → (Bx) = (𝐺‘(Bx))) → (x On → ((x On B Fn On) → (y x (By) = (𝐹y) → (Bx) = (𝐹x)))))
3534exp4a 348 . . . . . . . . . . 11 ((x On → (Bx) = (𝐺‘(Bx))) → (x On → (x On → (B Fn On → (y x (By) = (𝐹y) → (Bx) = (𝐹x))))))
3635pm2.43d 44 . . . . . . . . . 10 ((x On → (Bx) = (𝐺‘(Bx))) → (x On → (B Fn On → (y x (By) = (𝐹y) → (Bx) = (𝐹x)))))
3711, 36syl 14 . . . . . . . . 9 (x On (Bx) = (𝐺‘(Bx)) → (x On → (B Fn On → (y x (By) = (𝐹y) → (Bx) = (𝐹x)))))
3837com3l 75 . . . . . . . 8 (x On → (B Fn On → (x On (Bx) = (𝐺‘(Bx)) → (y x (By) = (𝐹y) → (Bx) = (𝐹x)))))
3938imp3a 242 . . . . . . 7 (x On → ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (y x (By) = (𝐹y) → (Bx) = (𝐹x))))
4039a2d 23 . . . . . 6 (x On → (((B Fn On x On (Bx) = (𝐺‘(Bx))) → y x (By) = (𝐹y)) → ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (Bx) = (𝐹x))))
4110, 40syl5bi 141 . . . . 5 (x On → (y x ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (By) = (𝐹y)) → ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (Bx) = (𝐹x))))
425, 9, 41tfis2f 4203 . . . 4 (x On → ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (Bx) = (𝐹x)))
4342com12 27 . . 3 ((B Fn On x On (Bx) = (𝐺‘(Bx))) → (x On → (Bx) = (𝐹x)))
443, 43ralrimi 2366 . 2 ((B Fn On x On (Bx) = (𝐺‘(Bx))) → x On (Bx) = (𝐹x))
45 eqfnfv 5157 . . . 4 ((B Fn On 𝐹 Fn On) → (B = 𝐹x On (Bx) = (𝐹x)))
4615, 45mpan2 403 . . 3 (B Fn On → (B = 𝐹x On (Bx) = (𝐹x)))
4746biimpar 281 . 2 ((B Fn On x On (Bx) = (𝐹x)) → B = 𝐹)
4844, 47syldan 266 1 ((B Fn On x On (Bx) = (𝐺‘(Bx))) → B = 𝐹)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   = wceq 1373   wcel 1375  wral 2282  Vcvv 2533  wss 2895  Oncon0 4024  cres 4240  Fun wfun 4790   Fn wfn 4791  cfv 4796  recscrecs 5806
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 1315  ax-7 1316  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-13 1386  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2004  ax-coll 3824  ax-sep 3827  ax-pow 3879  ax-pr 3896  ax-un 4093  ax-setind 4174
This theorem depends on definitions:  df-bi 110  df-3an 877  df-tru 1231  df-fal 1232  df-nf 1329  df-sb 1628  df-eu 1884  df-mo 1885  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2287  df-rex 2288  df-reu 2289  df-rab 2291  df-v 2535  df-sbc 2740  df-csb 2829  df-dif 2898  df-un 2900  df-in 2902  df-ss 2909  df-nul 3203  df-pw 3313  df-sn 3333  df-pr 3334  df-op 3336  df-uni 3533  df-iun 3611  df-br 3717  df-opab 3771  df-mpt 3772  df-tr 3807  df-id 3983  df-iord 4027  df-on 4028  df-suc 4031  df-xp 4244  df-rel 4245  df-cnv 4246  df-co 4247  df-dm 4248  df-rn 4249  df-res 4250  df-ima 4251  df-iota 4761  df-fun 4798  df-fn 4799  df-f 4800  df-f1 4801  df-fo 4802  df-f1o 4803  df-fv 4804  df-recs 5807
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator