isf32lem5

Description: Lemma for isfin3-2 . There are infinite decrease points. (Contributed by Stefan O'Rear, 5-Nov-2014)

	Ref	Expression
Hypotheses	isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
	isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
	isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
	isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
Assertion	isf32lem5	$⊢ φ \to \neg S \in Fin$

Proof

Step	Hyp	Ref	Expression
1		isf32lem.a	$⊢ φ \to F : ω ⟶ 𝒫 G$
2		isf32lem.b	$⊢ φ \to \forall x \in ω F (suc x) \subseteq F (x)$
3		isf32lem.c	$⊢ φ \to \neg ⋂ ran F \in ran F$
4		isf32lem.d	$⊢ S = \{y \in ω \| F (suc y) \subset F (y)\}$
5	1 2 3	isf32lem2	$⊢ (φ \land a \in ω) \to \exists b \in ω (a \in b \land F (suc b) \subset F (b))$
6	5	ralrimiva	$⊢ φ \to \forall a \in ω \exists b \in ω (a \in b \land F (suc b) \subset F (b))$
7	4	ssrab3	$⊢ S \subseteq ω$
8		nnunifi	$⊢ (S \subseteq ω \land S \in Fin) \to ⋃ S \in ω$
9	7 8	mpan	$⊢ S \in Fin \to ⋃ S \in ω$
10	9	adantl	$⊢ (φ \land S \in Fin) \to ⋃ S \in ω$
11		elssuni	$⊢ b \in S \to b \subseteq ⋃ S$
12		nnon	$⊢ b \in ω \to b \in On$
13		omsson	$⊢ ω \subseteq On$
14	13 10	sselid	$⊢ (φ \land S \in Fin) \to ⋃ S \in On$
15		ontri1	$⊢ (b \in On \land ⋃ S \in On) \to (b \subseteq ⋃ S \leftrightarrow \neg ⋃ S \in b)$
16	12 14 15	syl2anr	$⊢ ((φ \land S \in Fin) \land b \in ω) \to (b \subseteq ⋃ S \leftrightarrow \neg ⋃ S \in b)$
17	11 16	imbitrid	$⊢ ((φ \land S \in Fin) \land b \in ω) \to (b \in S \to \neg ⋃ S \in b)$
18	17	con2d	$⊢ ((φ \land S \in Fin) \land b \in ω) \to (⋃ S \in b \to \neg b \in S)$
19	18	impr	$⊢ ((φ \land S \in Fin) \land (b \in ω \land ⋃ S \in b)) \to \neg b \in S$
20	4	eleq2i	$⊢ b \in S \leftrightarrow b \in \{y \in ω \| F (suc y) \subset F (y)\}$
21	19 20	sylnib	$⊢ ((φ \land S \in Fin) \land (b \in ω \land ⋃ S \in b)) \to \neg b \in \{y \in ω \| F (suc y) \subset F (y)\}$
22		suceq	$⊢ y = b \to suc y = suc b$
23	22	fveq2d	$⊢ y = b \to F (suc y) = F (suc b)$
24		fveq2	$⊢ y = b \to F (y) = F (b)$
25	23 24	psseq12d	$⊢ y = b \to (F (suc y) \subset F (y) \leftrightarrow F (suc b) \subset F (b))$
26	25	elrab3	$⊢ b \in ω \to (b \in \{y \in ω \| F (suc y) \subset F (y)\} \leftrightarrow F (suc b) \subset F (b))$
27	26	ad2antrl	$⊢ ((φ \land S \in Fin) \land (b \in ω \land ⋃ S \in b)) \to (b \in \{y \in ω \| F (suc y) \subset F (y)\} \leftrightarrow F (suc b) \subset F (b))$
28	21 27	mtbid	$⊢ ((φ \land S \in Fin) \land (b \in ω \land ⋃ S \in b)) \to \neg F (suc b) \subset F (b)$
29	28	expr	$⊢ ((φ \land S \in Fin) \land b \in ω) \to (⋃ S \in b \to \neg F (suc b) \subset F (b))$
30		imnan	$⊢ (⋃ S \in b \to \neg F (suc b) \subset F (b)) \leftrightarrow \neg (⋃ S \in b \land F (suc b) \subset F (b))$
31	29 30	sylib	$⊢ ((φ \land S \in Fin) \land b \in ω) \to \neg (⋃ S \in b \land F (suc b) \subset F (b))$
32	31	nrexdv	$⊢ (φ \land S \in Fin) \to \neg \exists b \in ω (⋃ S \in b \land F (suc b) \subset F (b))$
33		eleq1	$⊢ a = ⋃ S \to (a \in b \leftrightarrow ⋃ S \in b)$
34	33	anbi1d	$⊢ a = ⋃ S \to ((a \in b \land F (suc b) \subset F (b)) \leftrightarrow (⋃ S \in b \land F (suc b) \subset F (b)))$
35	34	rexbidv	$⊢ a = ⋃ S \to (\exists b \in ω (a \in b \land F (suc b) \subset F (b)) \leftrightarrow \exists b \in ω (⋃ S \in b \land F (suc b) \subset F (b)))$
36	35	notbid	$⊢ a = ⋃ S \to (\neg \exists b \in ω (a \in b \land F (suc b) \subset F (b)) \leftrightarrow \neg \exists b \in ω (⋃ S \in b \land F (suc b) \subset F (b)))$
37	36	rspcev	$⊢ (⋃ S \in ω \land \neg \exists b \in ω (⋃ S \in b \land F (suc b) \subset F (b))) \to \exists a \in ω \neg \exists b \in ω (a \in b \land F (suc b) \subset F (b))$
38	10 32 37	syl2anc	$⊢ (φ \land S \in Fin) \to \exists a \in ω \neg \exists b \in ω (a \in b \land F (suc b) \subset F (b))$
39		rexnal	$⊢ \exists a \in ω \neg \exists b \in ω (a \in b \land F (suc b) \subset F (b)) \leftrightarrow \neg \forall a \in ω \exists b \in ω (a \in b \land F (suc b) \subset F (b))$
40	38 39	sylib	$⊢ (φ \land S \in Fin) \to \neg \forall a \in ω \exists b \in ω (a \in b \land F (suc b) \subset F (b))$
41	40	ex	$⊢ φ \to (S \in Fin \to \neg \forall a \in ω \exists b \in ω (a \in b \land F (suc b) \subset F (b)))$
42	6 41	mt2d	$⊢ φ \to \neg S \in Fin$

Metamath Proof Explorer

Theorem isf32lem5

Proof