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 \to {Inacc}_{𝑤} = Inacc$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (GCH = V \land x \in {Inacc}_{𝑤}) \to x \in {Inacc}_{𝑤}$
2		idd	$⊢ (GCH = V \land x \in {Inacc}_{𝑤}) \to (x \neq \emptyset \to x \neq \emptyset)$
3		idd	$⊢ (GCH = V \land x \in {Inacc}_{𝑤}) \to (cf (x) = x \to cf (x) = x)$
4		pwfi	$⊢ y \in Fin \leftrightarrow 𝒫 y \in Fin$
5		isfinite	$⊢ 𝒫 y \in Fin \leftrightarrow 𝒫 y ≺ ω$
6		winainf	$⊢ x \in {Inacc}_{𝑤} \to ω \subseteq x$
7		ssdomg	$⊢ x \in {Inacc}_{𝑤} \to (ω \subseteq x \to ω ≼ x)$
8	6 7	mpd	$⊢ x \in {Inacc}_{𝑤} \to ω ≼ x$
9		sdomdomtr	$⊢ (𝒫 y ≺ ω \land ω ≼ x) \to 𝒫 y ≺ x$
10	9	expcom	$⊢ ω ≼ x \to (𝒫 y ≺ ω \to 𝒫 y ≺ x)$
11	8 10	syl	$⊢ x \in {Inacc}_{𝑤} \to (𝒫 y ≺ ω \to 𝒫 y ≺ x)$
12	5 11	biimtrid	$⊢ x \in {Inacc}_{𝑤} \to (𝒫 y \in Fin \to 𝒫 y ≺ x)$
13	4 12	biimtrid	$⊢ x \in {Inacc}_{𝑤} \to (y \in Fin \to 𝒫 y ≺ x)$
14	13	ad3antlr	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land z \in x) \to (y \in Fin \to 𝒫 y ≺ x)$
15	14	a1dd	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land z \in x) \to (y \in Fin \to (y ≺ z \to 𝒫 y ≺ x))$
16		vex	$⊢ y \in V$
17		simplll	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to GCH = V$
18	16 17	eleqtrrid	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to y \in GCH$
19		simprr	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to \neg y \in Fin$
20		gchinf	$⊢ (y \in GCH \land \neg y \in Fin) \to ω ≼ y$
21	18 19 20	syl2anc	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to ω ≼ y$
22		vex	$⊢ z \in V$
23	22 17	eleqtrrid	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to z \in GCH$
24		gchpwdom	$⊢ (ω ≼ y \land y \in GCH \land z \in GCH) \to (y ≺ z \leftrightarrow 𝒫 y ≼ z)$
25	21 18 23 24	syl3anc	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to (y ≺ z \leftrightarrow 𝒫 y ≼ z)$
26		winacard	$⊢ x \in {Inacc}_{𝑤} \to card (x) = x$
27		iscard	$⊢ card (x) = x \leftrightarrow (x \in On \land \forall z \in x z ≺ x)$
28	27	simprbi	$⊢ card (x) = x \to \forall z \in x z ≺ x$
29	26 28	syl	$⊢ x \in {Inacc}_{𝑤} \to \forall z \in x z ≺ x$
30	29	ad2antlr	$⊢ ((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \to \forall z \in x z ≺ x$
31	30	r19.21bi	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land z \in x) \to z ≺ x$
32		domsdomtr	$⊢ (𝒫 y ≼ z \land z ≺ x) \to 𝒫 y ≺ x$
33	32	expcom	$⊢ z ≺ x \to (𝒫 y ≼ z \to 𝒫 y ≺ x)$
34	31 33	syl	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land z \in x) \to (𝒫 y ≼ z \to 𝒫 y ≺ x)$
35	34	adantrr	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to (𝒫 y ≼ z \to 𝒫 y ≺ x)$
36	25 35	sylbid	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land (z \in x \land \neg y \in Fin)) \to (y ≺ z \to 𝒫 y ≺ x)$
37	36	expr	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land z \in x) \to (\neg y \in Fin \to (y ≺ z \to 𝒫 y ≺ x))$
38	15 37	pm2.61d	$⊢ (((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \land z \in x) \to (y ≺ z \to 𝒫 y ≺ x)$
39	38	rexlimdva	$⊢ ((GCH = V \land x \in {Inacc}_{𝑤}) \land y \in x) \to (\exists z \in x y ≺ z \to 𝒫 y ≺ x)$
40	39	ralimdva	$⊢ (GCH = V \land x \in {Inacc}_{𝑤}) \to (\forall y \in x \exists z \in x y ≺ z \to \forall y \in x 𝒫 y ≺ x)$
41	2 3 40	3anim123d	$⊢ (GCH = V \land x \in {Inacc}_{𝑤}) \to ((x \neq \emptyset \land cf (x) = x \land \forall y \in x \exists z \in x y ≺ z) \to (x \neq \emptyset \land cf (x) = x \land \forall y \in x 𝒫 y ≺ x))$
42		elwina	$⊢ x \in {Inacc}_{𝑤} \leftrightarrow (x \neq \emptyset \land cf (x) = x \land \forall y \in x \exists z \in x y ≺ z)$
43		elina	$⊢ x \in Inacc \leftrightarrow (x \neq \emptyset \land cf (x) = x \land \forall y \in x 𝒫 y ≺ x)$
44	41 42 43	3imtr4g	$⊢ (GCH = V \land x \in {Inacc}_{𝑤}) \to (x \in {Inacc}_{𝑤} \to x \in Inacc)$
45	1 44	mpd	$⊢ (GCH = V \land x \in {Inacc}_{𝑤}) \to x \in Inacc$
46	45	ex	$⊢ GCH = V \to (x \in {Inacc}_{𝑤} \to x \in Inacc)$
47		inawina	$⊢ x \in Inacc \to x \in {Inacc}_{𝑤}$
48	46 47	impbid1	$⊢ GCH = V \to (x \in {Inacc}_{𝑤} \leftrightarrow x \in Inacc)$
49	48	eqrdv	$⊢ GCH = V \to {Inacc}_{𝑤} = Inacc$

Metamath Proof Explorer

Theorem gchina

Proof