winainflem

Description: A weakly inaccessible cardinal is infinite. (Contributed by Mario Carneiro, 29-May-2014)

		Ref	Expression
	Assertion	winainflem	$⊢ (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y) \to ω \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		nn0suc	$⊢ A \in ω \to (A = \emptyset \lor \exists z \in ω A = suc z)$
2		simp1	$⊢ (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y) \to A \neq \emptyset$
3	2	necon2bi	$⊢ A = \emptyset \to \neg (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y)$
4		vex	$⊢ z \in V$
5	4	sucid	$⊢ z \in suc z$
6		eleq2	$⊢ A = suc z \to (z \in A \leftrightarrow z \in suc z)$
7	5 6	mpbiri	$⊢ A = suc z \to z \in A$
8	7	adantl	$⊢ (z \in ω \land A = suc z) \to z \in A$
9		breq1	$⊢ x = z \to (x ≺ y \leftrightarrow z ≺ y)$
10	9	rexbidv	$⊢ x = z \to (\exists y \in A x ≺ y \leftrightarrow \exists y \in A z ≺ y)$
11		breq2	$⊢ y = w \to (z ≺ y \leftrightarrow z ≺ w)$
12	11	cbvrexvw	$⊢ \exists y \in A z ≺ y \leftrightarrow \exists w \in A z ≺ w$
13	10 12	bitrdi	$⊢ x = z \to (\exists y \in A x ≺ y \leftrightarrow \exists w \in A z ≺ w)$
14	13	rspcv	$⊢ z \in A \to (\forall x \in A \exists y \in A x ≺ y \to \exists w \in A z ≺ w)$
15	8 14	syl	$⊢ (z \in ω \land A = suc z) \to (\forall x \in A \exists y \in A x ≺ y \to \exists w \in A z ≺ w)$
16		eleq2	$⊢ A = suc z \to (w \in A \leftrightarrow w \in suc z)$
17	16	biimpa	$⊢ (A = suc z \land w \in A) \to w \in suc z$
18	17	3ad2antl2	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to w \in suc z$
19		nnon	$⊢ z \in ω \to z \in On$
20		onsuc	$⊢ z \in On \to suc z \in On$
21	19 20	syl	$⊢ z \in ω \to suc z \in On$
22		eleq1	$⊢ A = suc z \to (A \in On \leftrightarrow suc z \in On)$
23	22	biimparc	$⊢ (suc z \in On \land A = suc z) \to A \in On$
24	21 23	sylan	$⊢ (z \in ω \land A = suc z) \to A \in On$
25	24	3adant3	$⊢ (z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \to A \in On$
26		onelon	$⊢ (A \in On \land w \in A) \to w \in On$
27	25 26	sylan	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to w \in On$
28		simpl1	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to z \in ω$
29	28 19	syl	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to z \in On$
30		onsssuc	$⊢ (w \in On \land z \in On) \to (w \subseteq z \leftrightarrow w \in suc z)$
31	27 29 30	syl2anc	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to (w \subseteq z \leftrightarrow w \in suc z)$
32	18 31	mpbird	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to w \subseteq z$
33		ssdomg	$⊢ z \in V \to (w \subseteq z \to w ≼ z)$
34	4 32 33	mpsyl	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to w ≼ z$
35		domnsym	$⊢ w ≼ z \to \neg z ≺ w$
36	34 35	syl	$⊢ ((z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \land w \in A) \to \neg z ≺ w$
37	36	nrexdv	$⊢ (z \in ω \land A = suc z \land \forall x \in A \exists y \in A x ≺ y) \to \neg \exists w \in A z ≺ w$
38	37	3expia	$⊢ (z \in ω \land A = suc z) \to (\forall x \in A \exists y \in A x ≺ y \to \neg \exists w \in A z ≺ w)$
39	15 38	pm2.65d	$⊢ (z \in ω \land A = suc z) \to \neg \forall x \in A \exists y \in A x ≺ y$
40	39	intn3an3d	$⊢ (z \in ω \land A = suc z) \to \neg (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y)$
41	40	rexlimiva	$⊢ \exists z \in ω A = suc z \to \neg (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y)$
42	3 41	jaoi	$⊢ (A = \emptyset \lor \exists z \in ω A = suc z) \to \neg (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y)$
43	1 42	syl	$⊢ A \in ω \to \neg (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y)$
44	43	con2i	$⊢ (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y) \to \neg A \in ω$
45		ordom	$⊢ Ord ω$
46		eloni	$⊢ A \in On \to Ord A$
47	46	3ad2ant2	$⊢ (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y) \to Ord A$
48		ordtri1	$⊢ (Ord ω \land Ord A) \to (ω \subseteq A \leftrightarrow \neg A \in ω)$
49	45 47 48	sylancr	$⊢ (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y) \to (ω \subseteq A \leftrightarrow \neg A \in ω)$
50	44 49	mpbird	$⊢ (A \neq \emptyset \land A \in On \land \forall x \in A \exists y \in A x ≺ y) \to ω \subseteq A$

Metamath Proof Explorer

Theorem winainflem

Proof