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

Theorem tfri3 5870
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 5868). 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 2332 . . . 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 1448 . . . . 5 x((B Fn On x On (Bx) = (𝐺‘(Bx))) → (By) = (𝐹y))
6 fveq2 5101 . . . . . . 7 (x = y → (Bx) = (By))
7 fveq2 5101 . . . . . . 7 (x = y → (𝐹x) = (𝐹y))
86, 7eqeq12d 2037 . . . . . 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 2373 . . . . . 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 2346 . . . . . . . . . 10 (x On (Bx) = (𝐺‘(Bx)) → (x On → (Bx) = (𝐺‘(Bx))))
12 onss 4167 . . . . . . . . . . . . . . . . . . 19 (x On → x ⊆ On)
13 tfri3.1 . . . . . . . . . . . . . . . . . . . . . 22 𝐹 = recs(𝐺)
14 tfri3.2 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐺 (𝐺x) V)
1513, 14tfri1 5868 . . . . . . . . . . . . . . . . . . . . 21 𝐹 Fn On
16 fvreseq 5194 . . . . . . . . . . . . . . . . . . . . 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 5101 . . . . . . . . . . . . . . . . . . . 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 5869 . . . . . . . . . . . . . . . . . . . 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 2035 . . . . . . . . . . . . . . . . . 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)))))
3938impd 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 4232 . . . 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 2367 . 2 ((B Fn On x On (Bx) = (𝐺‘(Bx))) → x On (Bx) = (𝐹x))
45 eqfnfv 5188 . . . 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 1228   wcel 1375  wral 2283  Vcvv 2534  wss 2893  Oncon0 4047  cres 4272  Fun wfun 4821   Fn wfn 4822  cfv 4827  recscrecs 5836
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 1364  ax-ie2 1365  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 2005  ax-coll 3845  ax-sep 3848  ax-pow 3900  ax-pr 3917  ax-un 4118  ax-setind 4202
This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-fal 1234  df-nf 1330  df-sb 1629  df-eu 1886  df-mo 1887  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-ne 2189  df-ral 2288  df-rex 2289  df-reu 2290  df-rab 2292  df-v 2536  df-sbc 2741  df-csb 2829  df-dif 2896  df-un 2898  df-in 2900  df-ss 2907  df-nul 3201  df-pw 3335  df-sn 3355  df-pr 3356  df-op 3358  df-uni 3554  df-iun 3632  df-br 3738  df-opab 3792  df-mpt 3793  df-tr 3828  df-id 4003  df-iord 4050  df-on 4052  df-suc 4055  df-xp 4276  df-rel 4277  df-cnv 4278  df-co 4279  df-dm 4280  df-rn 4281  df-res 4282  df-ima 4283  df-iota 4792  df-fun 4829  df-fn 4830  df-f 4831  df-f1 4832  df-fo 4833  df-f1o 4834  df-fv 4835  df-recs 5837
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator