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 )