limsucncmpi

Description: The successor of a limit ordinal is not compact. (Contributed by Chen-Pang He, 20-Oct-2015)

		Ref	Expression
	Hypothesis	limsucncmpi.1	$⊢ Lim A$
	Assertion	limsucncmpi	$⊢ \neg suc A \in Comp$

Proof

Step	Hyp	Ref	Expression
1		limsucncmpi.1	$⊢ Lim A$
2		elex	$⊢ suc A \in Top \to suc A \in V$
3		sucexb	$⊢ A \in V \leftrightarrow suc A \in V$
4	2 3	sylibr	$⊢ suc A \in Top \to A \in V$
5		sssucid	$⊢ A \subseteq suc A$
6		elpwg	$⊢ A \in V \to (A \in 𝒫 suc A \leftrightarrow A \subseteq suc A)$
7	5 6	mpbiri	$⊢ A \in V \to A \in 𝒫 suc A$
8		limuni	$⊢ Lim A \to A = ⋃ A$
9	1 8	ax-mp	$⊢ A = ⋃ A$
10		elin	$⊢ z \in (𝒫 A \cap Fin) \leftrightarrow (z \in 𝒫 A \land z \in Fin)$
11		elpwi	$⊢ z \in 𝒫 A \to z \subseteq A$
12	11	anim1i	$⊢ (z \in 𝒫 A \land z \in Fin) \to (z \subseteq A \land z \in Fin)$
13	10 12	sylbi	$⊢ z \in (𝒫 A \cap Fin) \to (z \subseteq A \land z \in Fin)$
14		nlim0	$⊢ \neg Lim \emptyset$
15	1 14	2th	$⊢ Lim A \leftrightarrow \neg Lim \emptyset$
16		xor3	$⊢ \neg (Lim A \leftrightarrow Lim \emptyset) \leftrightarrow (Lim A \leftrightarrow \neg Lim \emptyset)$
17	15 16	mpbir	$⊢ \neg (Lim A \leftrightarrow Lim \emptyset)$
18		limeq	$⊢ A = \emptyset \to (Lim A \leftrightarrow Lim \emptyset)$
19	18	necon3bi	$⊢ \neg (Lim A \leftrightarrow Lim \emptyset) \to A \neq \emptyset$
20	17 19	ax-mp	$⊢ A \neq \emptyset$
21		uni0	$⊢ ⋃ \emptyset = \emptyset$
22	20 21	neeqtrri	$⊢ A \neq ⋃ \emptyset$
23		unieq	$⊢ z = \emptyset \to ⋃ z = ⋃ \emptyset$
24	23	neeq2d	$⊢ z = \emptyset \to (A \neq ⋃ z \leftrightarrow A \neq ⋃ \emptyset)$
25	22 24	mpbiri	$⊢ z = \emptyset \to A \neq ⋃ z$
26	25	a1i	$⊢ (z \subseteq A \land z \in Fin) \to (z = \emptyset \to A \neq ⋃ z)$
27		limord	$⊢ Lim A \to Ord A$
28		ordsson	$⊢ Ord A \to A \subseteq On$
29	1 27 28	mp2b	$⊢ A \subseteq On$
30		sstr2	$⊢ z \subseteq A \to (A \subseteq On \to z \subseteq On)$
31	29 30	mpi	$⊢ z \subseteq A \to z \subseteq On$
32		ordunifi	$⊢ (z \subseteq On \land z \in Fin \land z \neq \emptyset) \to ⋃ z \in z$
33	32	3expia	$⊢ (z \subseteq On \land z \in Fin) \to (z \neq \emptyset \to ⋃ z \in z)$
34	31 33	sylan	$⊢ (z \subseteq A \land z \in Fin) \to (z \neq \emptyset \to ⋃ z \in z)$
35		ssel	$⊢ z \subseteq A \to (⋃ z \in z \to ⋃ z \in A)$
36	1 27	ax-mp	$⊢ Ord A$
37		nordeq	$⊢ (Ord A \land ⋃ z \in A) \to A \neq ⋃ z$
38	36 37	mpan	$⊢ ⋃ z \in A \to A \neq ⋃ z$
39	35 38	syl6	$⊢ z \subseteq A \to (⋃ z \in z \to A \neq ⋃ z)$
40	39	adantr	$⊢ (z \subseteq A \land z \in Fin) \to (⋃ z \in z \to A \neq ⋃ z)$
41	34 40	syld	$⊢ (z \subseteq A \land z \in Fin) \to (z \neq \emptyset \to A \neq ⋃ z)$
42	26 41	pm2.61dne	$⊢ (z \subseteq A \land z \in Fin) \to A \neq ⋃ z$
43	13 42	syl	$⊢ z \in (𝒫 A \cap Fin) \to A \neq ⋃ z$
44	43	neneqd	$⊢ z \in (𝒫 A \cap Fin) \to \neg A = ⋃ z$
45	44	nrex	$⊢ \neg \exists z \in (𝒫 A \cap Fin) A = ⋃ z$
46		unieq	$⊢ y = A \to ⋃ y = ⋃ A$
47	46	eqeq2d	$⊢ y = A \to (A = ⋃ y \leftrightarrow A = ⋃ A)$
48		pweq	$⊢ y = A \to 𝒫 y = 𝒫 A$
49	48	ineq1d	$⊢ y = A \to 𝒫 y \cap Fin = 𝒫 A \cap Fin$
50	49	rexeqdv	$⊢ y = A \to (\exists z \in (𝒫 y \cap Fin) A = ⋃ z \leftrightarrow \exists z \in (𝒫 A \cap Fin) A = ⋃ z)$
51	50	notbid	$⊢ y = A \to (\neg \exists z \in (𝒫 y \cap Fin) A = ⋃ z \leftrightarrow \neg \exists z \in (𝒫 A \cap Fin) A = ⋃ z)$
52	47 51	anbi12d	$⊢ y = A \to ((A = ⋃ y \land \neg \exists z \in (𝒫 y \cap Fin) A = ⋃ z) \leftrightarrow (A = ⋃ A \land \neg \exists z \in (𝒫 A \cap Fin) A = ⋃ z))$
53	52	rspcev	$⊢ (A \in 𝒫 suc A \land (A = ⋃ A \land \neg \exists z \in (𝒫 A \cap Fin) A = ⋃ z)) \to \exists y \in 𝒫 suc A (A = ⋃ y \land \neg \exists z \in (𝒫 y \cap Fin) A = ⋃ z)$
54	9 45 53	mpanr12	$⊢ A \in 𝒫 suc A \to \exists y \in 𝒫 suc A (A = ⋃ y \land \neg \exists z \in (𝒫 y \cap Fin) A = ⋃ z)$
55		rexanali	$⊢ \exists y \in 𝒫 suc A (A = ⋃ y \land \neg \exists z \in (𝒫 y \cap Fin) A = ⋃ z) \leftrightarrow \neg \forall y \in 𝒫 suc A (A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) A = ⋃ z)$
56	54 55	sylib	$⊢ A \in 𝒫 suc A \to \neg \forall y \in 𝒫 suc A (A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) A = ⋃ z)$
57	4 7 56	3syl	$⊢ suc A \in Top \to \neg \forall y \in 𝒫 suc A (A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) A = ⋃ z)$
58		imnan	$⊢ (suc A \in Top \to \neg \forall y \in 𝒫 suc A (A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) A = ⋃ z)) \leftrightarrow \neg (suc A \in Top \land \forall y \in 𝒫 suc A (A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) A = ⋃ z))$
59	57 58	mpbi	$⊢ \neg (suc A \in Top \land \forall y \in 𝒫 suc A (A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) A = ⋃ z))$
60		ordunisuc	$⊢ Ord A \to ⋃ suc A = A$
61	1 27 60	mp2b	$⊢ ⋃ suc A = A$
62	61	eqcomi	$⊢ A = ⋃ suc A$
63	62	iscmp	$⊢ suc A \in Comp \leftrightarrow (suc A \in Top \land \forall y \in 𝒫 suc A (A = ⋃ y \to \exists z \in (𝒫 y \cap Fin) A = ⋃ z))$
64	59 63	mtbir	$⊢ \neg suc A \in Comp$

Metamath Proof Explorer

Theorem limsucncmpi

Proof