MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inatsk Structured version   Visualization version   GIF version

Theorem inatsk 10178
Description: (𝑅1𝐴) for 𝐴 a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013.)
Assertion
Ref Expression
inatsk (𝐴 ∈ Inacc → (𝑅1𝐴) ∈ Tarski)

Proof of Theorem inatsk
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 inawina 10090 . . . . . 6 (𝐴 ∈ Inacc → 𝐴 ∈ Inaccw)
2 winaon 10088 . . . . . . . . . 10 (𝐴 ∈ Inaccw𝐴 ∈ On)
3 winalim 10095 . . . . . . . . . 10 (𝐴 ∈ Inaccw → Lim 𝐴)
4 r1lim 9179 . . . . . . . . . 10 ((𝐴 ∈ On ∧ Lim 𝐴) → (𝑅1𝐴) = 𝑦𝐴 (𝑅1𝑦))
52, 3, 4syl2anc 586 . . . . . . . . 9 (𝐴 ∈ Inaccw → (𝑅1𝐴) = 𝑦𝐴 (𝑅1𝑦))
65eleq2d 2896 . . . . . . . 8 (𝐴 ∈ Inaccw → (𝑥 ∈ (𝑅1𝐴) ↔ 𝑥 𝑦𝐴 (𝑅1𝑦)))
7 eliun 4899 . . . . . . . 8 (𝑥 𝑦𝐴 (𝑅1𝑦) ↔ ∃𝑦𝐴 𝑥 ∈ (𝑅1𝑦))
86, 7syl6bb 289 . . . . . . 7 (𝐴 ∈ Inaccw → (𝑥 ∈ (𝑅1𝐴) ↔ ∃𝑦𝐴 𝑥 ∈ (𝑅1𝑦)))
9 onelon 6192 . . . . . . . . . . 11 ((𝐴 ∈ On ∧ 𝑦𝐴) → 𝑦 ∈ On)
102, 9sylan 582 . . . . . . . . . 10 ((𝐴 ∈ Inaccw𝑦𝐴) → 𝑦 ∈ On)
11 r1pw 9252 . . . . . . . . . 10 (𝑦 ∈ On → (𝑥 ∈ (𝑅1𝑦) ↔ 𝒫 𝑥 ∈ (𝑅1‘suc 𝑦)))
1210, 11syl 17 . . . . . . . . 9 ((𝐴 ∈ Inaccw𝑦𝐴) → (𝑥 ∈ (𝑅1𝑦) ↔ 𝒫 𝑥 ∈ (𝑅1‘suc 𝑦)))
13 limsuc 7542 . . . . . . . . . . . . 13 (Lim 𝐴 → (𝑦𝐴 ↔ suc 𝑦𝐴))
143, 13syl 17 . . . . . . . . . . . 12 (𝐴 ∈ Inaccw → (𝑦𝐴 ↔ suc 𝑦𝐴))
15 r1ord2 9188 . . . . . . . . . . . . 13 (𝐴 ∈ On → (suc 𝑦𝐴 → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝐴)))
162, 15syl 17 . . . . . . . . . . . 12 (𝐴 ∈ Inaccw → (suc 𝑦𝐴 → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝐴)))
1714, 16sylbid 242 . . . . . . . . . . 11 (𝐴 ∈ Inaccw → (𝑦𝐴 → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝐴)))
1817imp 409 . . . . . . . . . 10 ((𝐴 ∈ Inaccw𝑦𝐴) → (𝑅1‘suc 𝑦) ⊆ (𝑅1𝐴))
1918sseld 3945 . . . . . . . . 9 ((𝐴 ∈ Inaccw𝑦𝐴) → (𝒫 𝑥 ∈ (𝑅1‘suc 𝑦) → 𝒫 𝑥 ∈ (𝑅1𝐴)))
2012, 19sylbid 242 . . . . . . . 8 ((𝐴 ∈ Inaccw𝑦𝐴) → (𝑥 ∈ (𝑅1𝑦) → 𝒫 𝑥 ∈ (𝑅1𝐴)))
2120rexlimdva 3271 . . . . . . 7 (𝐴 ∈ Inaccw → (∃𝑦𝐴 𝑥 ∈ (𝑅1𝑦) → 𝒫 𝑥 ∈ (𝑅1𝐴)))
228, 21sylbid 242 . . . . . 6 (𝐴 ∈ Inaccw → (𝑥 ∈ (𝑅1𝐴) → 𝒫 𝑥 ∈ (𝑅1𝐴)))
231, 22syl 17 . . . . 5 (𝐴 ∈ Inacc → (𝑥 ∈ (𝑅1𝐴) → 𝒫 𝑥 ∈ (𝑅1𝐴)))
2423imp 409 . . . 4 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ (𝑅1𝐴)) → 𝒫 𝑥 ∈ (𝑅1𝐴))
25 elssuni 4844 . . . . 5 (𝒫 𝑥 ∈ (𝑅1𝐴) → 𝒫 𝑥 (𝑅1𝐴))
26 r1tr2 9184 . . . . 5 (𝑅1𝐴) ⊆ (𝑅1𝐴)
2725, 26sstrdi 3958 . . . 4 (𝒫 𝑥 ∈ (𝑅1𝐴) → 𝒫 𝑥 ⊆ (𝑅1𝐴))
2824, 27jccil 525 . . 3 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ (𝑅1𝐴)) → (𝒫 𝑥 ⊆ (𝑅1𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1𝐴)))
2928ralrimiva 3169 . 2 (𝐴 ∈ Inacc → ∀𝑥 ∈ (𝑅1𝐴)(𝒫 𝑥 ⊆ (𝑅1𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1𝐴)))
301, 2syl 17 . . . . . . . . 9 (𝐴 ∈ Inacc → 𝐴 ∈ On)
31 r1suc 9177 . . . . . . . . . 10 (𝐴 ∈ On → (𝑅1‘suc 𝐴) = 𝒫 (𝑅1𝐴))
3231eleq2d 2896 . . . . . . . . 9 (𝐴 ∈ On → (𝑥 ∈ (𝑅1‘suc 𝐴) ↔ 𝑥 ∈ 𝒫 (𝑅1𝐴)))
3330, 32syl 17 . . . . . . . 8 (𝐴 ∈ Inacc → (𝑥 ∈ (𝑅1‘suc 𝐴) ↔ 𝑥 ∈ 𝒫 (𝑅1𝐴)))
34 rankr1ai 9205 . . . . . . . 8 (𝑥 ∈ (𝑅1‘suc 𝐴) → (rank‘𝑥) ∈ suc 𝐴)
3533, 34syl6bir 256 . . . . . . 7 (𝐴 ∈ Inacc → (𝑥 ∈ 𝒫 (𝑅1𝐴) → (rank‘𝑥) ∈ suc 𝐴))
3635imp 409 . . . . . 6 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → (rank‘𝑥) ∈ suc 𝐴)
37 fvex 6659 . . . . . . 7 (rank‘𝑥) ∈ V
3837elsuc 6236 . . . . . 6 ((rank‘𝑥) ∈ suc 𝐴 ↔ ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴))
3936, 38sylib 220 . . . . 5 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → ((rank‘𝑥) ∈ 𝐴 ∨ (rank‘𝑥) = 𝐴))
4039orcomd 867 . . . 4 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → ((rank‘𝑥) = 𝐴 ∨ (rank‘𝑥) ∈ 𝐴))
41 fvex 6659 . . . . . . . 8 (𝑅1𝐴) ∈ V
42 elpwi 4524 . . . . . . . . 9 (𝑥 ∈ 𝒫 (𝑅1𝐴) → 𝑥 ⊆ (𝑅1𝐴))
4342ad2antlr 725 . . . . . . . 8 (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) ∧ (rank‘𝑥) = 𝐴) → 𝑥 ⊆ (𝑅1𝐴))
44 ssdomg 8533 . . . . . . . 8 ((𝑅1𝐴) ∈ V → (𝑥 ⊆ (𝑅1𝐴) → 𝑥 ≼ (𝑅1𝐴)))
4541, 43, 44mpsyl 68 . . . . . . 7 (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) ∧ (rank‘𝑥) = 𝐴) → 𝑥 ≼ (𝑅1𝐴))
46 rankcf 10177 . . . . . . . . . 10 ¬ 𝑥 ≺ (cf‘(rank‘𝑥))
47 fveq2 6646 . . . . . . . . . . . 12 ((rank‘𝑥) = 𝐴 → (cf‘(rank‘𝑥)) = (cf‘𝐴))
48 elina 10087 . . . . . . . . . . . . 13 (𝐴 ∈ Inacc ↔ (𝐴 ≠ ∅ ∧ (cf‘𝐴) = 𝐴 ∧ ∀𝑥𝐴 𝒫 𝑥𝐴))
4948simp2bi 1142 . . . . . . . . . . . 12 (𝐴 ∈ Inacc → (cf‘𝐴) = 𝐴)
5047, 49sylan9eqr 2877 . . . . . . . . . . 11 ((𝐴 ∈ Inacc ∧ (rank‘𝑥) = 𝐴) → (cf‘(rank‘𝑥)) = 𝐴)
5150breq2d 5054 . . . . . . . . . 10 ((𝐴 ∈ Inacc ∧ (rank‘𝑥) = 𝐴) → (𝑥 ≺ (cf‘(rank‘𝑥)) ↔ 𝑥𝐴))
5246, 51mtbii 328 . . . . . . . . 9 ((𝐴 ∈ Inacc ∧ (rank‘𝑥) = 𝐴) → ¬ 𝑥𝐴)
53 inar1 10175 . . . . . . . . . . 11 (𝐴 ∈ Inacc → (𝑅1𝐴) ≈ 𝐴)
54 sdomentr 8629 . . . . . . . . . . . 12 ((𝑥 ≺ (𝑅1𝐴) ∧ (𝑅1𝐴) ≈ 𝐴) → 𝑥𝐴)
5554expcom 416 . . . . . . . . . . 11 ((𝑅1𝐴) ≈ 𝐴 → (𝑥 ≺ (𝑅1𝐴) → 𝑥𝐴))
5653, 55syl 17 . . . . . . . . . 10 (𝐴 ∈ Inacc → (𝑥 ≺ (𝑅1𝐴) → 𝑥𝐴))
5756adantr 483 . . . . . . . . 9 ((𝐴 ∈ Inacc ∧ (rank‘𝑥) = 𝐴) → (𝑥 ≺ (𝑅1𝐴) → 𝑥𝐴))
5852, 57mtod 200 . . . . . . . 8 ((𝐴 ∈ Inacc ∧ (rank‘𝑥) = 𝐴) → ¬ 𝑥 ≺ (𝑅1𝐴))
5958adantlr 713 . . . . . . 7 (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) ∧ (rank‘𝑥) = 𝐴) → ¬ 𝑥 ≺ (𝑅1𝐴))
60 bren2 8518 . . . . . . 7 (𝑥 ≈ (𝑅1𝐴) ↔ (𝑥 ≼ (𝑅1𝐴) ∧ ¬ 𝑥 ≺ (𝑅1𝐴)))
6145, 59, 60sylanbrc 585 . . . . . 6 (((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) ∧ (rank‘𝑥) = 𝐴) → 𝑥 ≈ (𝑅1𝐴))
6261ex 415 . . . . 5 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → ((rank‘𝑥) = 𝐴𝑥 ≈ (𝑅1𝐴)))
63 r1elwf 9203 . . . . . . . . 9 (𝑥 ∈ (𝑅1‘suc 𝐴) → 𝑥 (𝑅1 “ On))
6433, 63syl6bir 256 . . . . . . . 8 (𝐴 ∈ Inacc → (𝑥 ∈ 𝒫 (𝑅1𝐴) → 𝑥 (𝑅1 “ On)))
6564imp 409 . . . . . . 7 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → 𝑥 (𝑅1 “ On))
66 r1fnon 9174 . . . . . . . . . 10 𝑅1 Fn On
67 fndm 6431 . . . . . . . . . 10 (𝑅1 Fn On → dom 𝑅1 = On)
6866, 67ax-mp 5 . . . . . . . . 9 dom 𝑅1 = On
6930, 68eleqtrrdi 2922 . . . . . . . 8 (𝐴 ∈ Inacc → 𝐴 ∈ dom 𝑅1)
7069adantr 483 . . . . . . 7 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → 𝐴 ∈ dom 𝑅1)
71 rankr1ag 9209 . . . . . . 7 ((𝑥 (𝑅1 “ On) ∧ 𝐴 ∈ dom 𝑅1) → (𝑥 ∈ (𝑅1𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
7265, 70, 71syl2anc 586 . . . . . 6 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → (𝑥 ∈ (𝑅1𝐴) ↔ (rank‘𝑥) ∈ 𝐴))
7372biimprd 250 . . . . 5 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → ((rank‘𝑥) ∈ 𝐴𝑥 ∈ (𝑅1𝐴)))
7462, 73orim12d 961 . . . 4 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → (((rank‘𝑥) = 𝐴 ∨ (rank‘𝑥) ∈ 𝐴) → (𝑥 ≈ (𝑅1𝐴) ∨ 𝑥 ∈ (𝑅1𝐴))))
7540, 74mpd 15 . . 3 ((𝐴 ∈ Inacc ∧ 𝑥 ∈ 𝒫 (𝑅1𝐴)) → (𝑥 ≈ (𝑅1𝐴) ∨ 𝑥 ∈ (𝑅1𝐴)))
7675ralrimiva 3169 . 2 (𝐴 ∈ Inacc → ∀𝑥 ∈ 𝒫 (𝑅1𝐴)(𝑥 ≈ (𝑅1𝐴) ∨ 𝑥 ∈ (𝑅1𝐴)))
77 eltsk2g 10151 . . 3 ((𝑅1𝐴) ∈ V → ((𝑅1𝐴) ∈ Tarski ↔ (∀𝑥 ∈ (𝑅1𝐴)(𝒫 𝑥 ⊆ (𝑅1𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1𝐴)) ∧ ∀𝑥 ∈ 𝒫 (𝑅1𝐴)(𝑥 ≈ (𝑅1𝐴) ∨ 𝑥 ∈ (𝑅1𝐴)))))
7841, 77ax-mp 5 . 2 ((𝑅1𝐴) ∈ Tarski ↔ (∀𝑥 ∈ (𝑅1𝐴)(𝒫 𝑥 ⊆ (𝑅1𝐴) ∧ 𝒫 𝑥 ∈ (𝑅1𝐴)) ∧ ∀𝑥 ∈ 𝒫 (𝑅1𝐴)(𝑥 ≈ (𝑅1𝐴) ∨ 𝑥 ∈ (𝑅1𝐴))))
7929, 76, 78sylanbrc 585 1 (𝐴 ∈ Inacc → (𝑅1𝐴) ∈ Tarski)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wo 843   = wceq 1537  wcel 2114  wne 3006  wral 3125  wrex 3126  Vcvv 3473  wss 3913  c0 4269  𝒫 cpw 4515   cuni 4814   ciun 4895   class class class wbr 5042  dom cdm 5531  cima 5534  Oncon0 6167  Lim wlim 6168  suc csuc 6169   Fn wfn 6326  cfv 6331  cen 8484  cdom 8485  csdm 8486  𝑅1cr1 9169  rankcrnk 9170  cfccf 9344  Inaccwcwina 10082  Inacccina 10083  Tarskictsk 10148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-ac2 9863
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-iin 4898  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-se 5491  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-isom 6340  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-2o 8081  df-oadd 8084  df-er 8267  df-map 8386  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-oi 8952  df-r1 9171  df-rank 9172  df-card 9346  df-cf 9348  df-acn 9349  df-ac 9520  df-wina 10084  df-ina 10085  df-tsk 10149
This theorem is referenced by:  r1omtsk  10179  r1tskina  10182  grutsk  10222  inagrud  40787
  Copyright terms: Public domain W3C validator