This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gchina

Description: Assuming the GCH, weakly and strongly inaccessible cardinals coincide. Theorem 11.20 of TakeutiZaring p. 106. (Contributed by Mario Carneiro, 5-Jun-2015)

Ref Expression
Assertion gchina ( GCH = V → Inaccw = Inacc )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) → 𝑥 ∈ Inaccw )
2 idd ⊢ ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) → ( 𝑥 ≠ ∅ → 𝑥 ≠ ∅ ) )
3 idd ⊢ ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) → ( ( cf ‘ 𝑥 ) = 𝑥 → ( cf ‘ 𝑥 ) = 𝑥 ) )
4 pwfi ⊢ ( 𝑦 ∈ Fin ↔ 𝒫 𝑦 ∈ Fin )
5 isfinite ⊢ ( 𝒫 𝑦 ∈ Fin ↔ 𝒫 𝑦 ≺ ω )
6 winainf ⊢ ( 𝑥 ∈ Inaccw → ω ⊆ 𝑥 )
7 ssdomg ⊢ ( 𝑥 ∈ Inaccw → ( ω ⊆ 𝑥 → ω ≼ 𝑥 ) )
8 6 7 mpd ⊢ ( 𝑥 ∈ Inaccw → ω ≼ 𝑥 )
9 sdomdomtr ⊢ ( ( 𝒫 𝑦 ≺ ω ∧ ω ≼ 𝑥 ) → 𝒫 𝑦 ≺ 𝑥 )
10 9 expcom ⊢ ( ω ≼ 𝑥 → ( 𝒫 𝑦 ≺ ω → 𝒫 𝑦 ≺ 𝑥 ) )
11 8 10 syl ⊢ ( 𝑥 ∈ Inaccw → ( 𝒫 𝑦 ≺ ω → 𝒫 𝑦 ≺ 𝑥 ) )
12 5 11 biimtrid ⊢ ( 𝑥 ∈ Inaccw → ( 𝒫 𝑦 ∈ Fin → 𝒫 𝑦 ≺ 𝑥 ) )
13 4 12 biimtrid ⊢ ( 𝑥 ∈ Inaccw → ( 𝑦 ∈ Fin → 𝒫 𝑦 ≺ 𝑥 ) )
14 13 ad3antlr ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑦 ∈ Fin → 𝒫 𝑦 ≺ 𝑥 ) )
15 14 a1dd ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑦 ∈ Fin → ( 𝑦 ≺ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) ) )
16 vex ⊢ 𝑦 ∈ V
17 simplll ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → GCH = V )
18 16 17 eleqtrrid ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → 𝑦 ∈ GCH )
19 simprr ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → ¬ 𝑦 ∈ Fin )
20 gchinf ⊢ ( ( 𝑦 ∈ GCH ∧ ¬ 𝑦 ∈ Fin ) → ω ≼ 𝑦 )
21 18 19 20 syl2anc ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → ω ≼ 𝑦 )
22 vex ⊢ 𝑧 ∈ V
23 22 17 eleqtrrid ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → 𝑧 ∈ GCH )
24 gchpwdom ⊢ ( ( ω ≼ 𝑦 ∧ 𝑦 ∈ GCH ∧ 𝑧 ∈ GCH ) → ( 𝑦 ≺ 𝑧 ↔ 𝒫 𝑦 ≼ 𝑧 ) )
25 21 18 23 24 syl3anc ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → ( 𝑦 ≺ 𝑧 ↔ 𝒫 𝑦 ≼ 𝑧 ) )
26 winacard ⊢ ( 𝑥 ∈ Inaccw → ( card ‘ 𝑥 ) = 𝑥 )
27 iscard ⊢ ( ( card ‘ 𝑥 ) = 𝑥 ↔ ( 𝑥 ∈ On ∧ ∀ 𝑧 ∈ 𝑥 𝑧 ≺ 𝑥 ) )
28 27 simprbi ⊢ ( ( card ‘ 𝑥 ) = 𝑥 → ∀ 𝑧 ∈ 𝑥 𝑧 ≺ 𝑥 )
29 26 28 syl ⊢ ( 𝑥 ∈ Inaccw → ∀ 𝑧 ∈ 𝑥 𝑧 ≺ 𝑥 )
30 29 ad2antlr ⊢ ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) → ∀ 𝑧 ∈ 𝑥 𝑧 ≺ 𝑥 )
31 30 r19.21bi ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ≺ 𝑥 )
32 domsdomtr ⊢ ( ( 𝒫 𝑦 ≼ 𝑧 ∧ 𝑧 ≺ 𝑥 ) → 𝒫 𝑦 ≺ 𝑥 )
33 32 expcom ⊢ ( 𝑧 ≺ 𝑥 → ( 𝒫 𝑦 ≼ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) )
34 31 33 syl ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝒫 𝑦 ≼ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) )
35 34 adantrr ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → ( 𝒫 𝑦 ≼ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) )
36 25 35 sylbid ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑧 ∈ 𝑥 ∧ ¬ 𝑦 ∈ Fin ) ) → ( 𝑦 ≺ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) )
37 36 expr ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → ( ¬ 𝑦 ∈ Fin → ( 𝑦 ≺ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) ) )
38 15 37 pm2.61d ⊢ ( ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑦 ≺ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) )
39 38 rexlimdva ⊢ ( ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 → 𝒫 𝑦 ≺ 𝑥 ) )
40 39 ralimdva ⊢ ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 → ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 ) )
41 2 3 40 3anim123d ⊢ ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) → ( ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) → ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 ) ) )
42 elwina ⊢ ( 𝑥 ∈ Inaccw ↔ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝑥 𝑦 ≺ 𝑧 ) )
43 elina ⊢ ( 𝑥 ∈ Inacc ↔ ( 𝑥 ≠ ∅ ∧ ( cf ‘ 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 𝒫 𝑦 ≺ 𝑥 ) )
44 41 42 43 3imtr4g ⊢ ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) → ( 𝑥 ∈ Inaccw → 𝑥 ∈ Inacc ) )
45 1 44 mpd ⊢ ( ( GCH = V ∧ 𝑥 ∈ Inaccw ) → 𝑥 ∈ Inacc )
46 45 ex ⊢ ( GCH = V → ( 𝑥 ∈ Inaccw → 𝑥 ∈ Inacc ) )
47 inawina ⊢ ( 𝑥 ∈ Inacc → 𝑥 ∈ Inaccw )
48 46 47 impbid1 ⊢ ( GCH = V → ( 𝑥 ∈ Inaccw ↔ 𝑥 ∈ Inacc ) )
49 48 eqrdv ⊢ ( GCH = V → Inaccw = Inacc )