isf32lem6

Description: Lemma for isfin3-2 . Each K value is nonempty. (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)\}$
	isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
	isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
Assertion	isf32lem6	$⊢ (φ \land A \in ω) \to K (A) \neq \emptyset$

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		isf32lem.e	$⊢ J = (u \in ω ⟼ (ι v \in S \| (v \cap S) \approx u))$
6		isf32lem.f	$⊢ K = (w \in S ⟼ F (w) ∖ F (suc w)) \circ J$
7	6	fveq1i	$⊢ K (A) = ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A)$
8	4	ssrab3	$⊢ S \subseteq ω$
9	1 2 3 4	isf32lem5	$⊢ φ \to \neg S \in Fin$
10	5	fin23lem22	$⊢ (S \subseteq ω \land \neg S \in Fin) \to J : ω \underset{1-1 onto}{⟶} S$
11	8 9 10	sylancr	$⊢ φ \to J : ω \underset{1-1 onto}{⟶} S$
12		f1of	$⊢ J : ω \underset{1-1 onto}{⟶} S \to J : ω ⟶ S$
13	11 12	syl	$⊢ φ \to J : ω ⟶ S$
14		fvco3	$⊢ (J : ω ⟶ S \land A \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (A))$
15	13 14	sylan	$⊢ (φ \land A \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = (w \in S ⟼ F (w) ∖ F (suc w)) (J (A))$
16	9	adantr	$⊢ (φ \land A \in ω) \to \neg S \in Fin$
17	8 16 10	sylancr	$⊢ (φ \land A \in ω) \to J : ω \underset{1-1 onto}{⟶} S$
18	17 12	syl	$⊢ (φ \land A \in ω) \to J : ω ⟶ S$
19		ffvelrn	$⊢ (J : ω ⟶ S \land A \in ω) \to J (A) \in S$
20	18 19	sylancom	$⊢ (φ \land A \in ω) \to J (A) \in S$
21		fveq2	$⊢ w = J (A) \to F (w) = F (J (A))$
22		suceq	$⊢ w = J (A) \to suc w = suc J (A)$
23	22	fveq2d	$⊢ w = J (A) \to F (suc w) = F (suc J (A))$
24	21 23	difeq12d	$⊢ w = J (A) \to F (w) ∖ F (suc w) = F (J (A)) ∖ F (suc J (A))$
25		eqid	$⊢ (w \in S ⟼ F (w) ∖ F (suc w)) = (w \in S ⟼ F (w) ∖ F (suc w))$
26		fvex	$⊢ F (J (A)) \in V$
27	26	difexi	$⊢ F (J (A)) ∖ F (suc J (A)) \in V$
28	24 25 27	fvmpt	$⊢ J (A) \in S \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (A)) = F (J (A)) ∖ F (suc J (A))$
29	20 28	syl	$⊢ (φ \land A \in ω) \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (A)) = F (J (A)) ∖ F (suc J (A))$
30	15 29	eqtrd	$⊢ (φ \land A \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = F (J (A)) ∖ F (suc J (A))$
31	7 30	syl5eq	$⊢ (φ \land A \in ω) \to K (A) = F (J (A)) ∖ F (suc J (A))$
32		suceq	$⊢ y = J (A) \to suc y = suc J (A)$
33	32	fveq2d	$⊢ y = J (A) \to F (suc y) = F (suc J (A))$
34		fveq2	$⊢ y = J (A) \to F (y) = F (J (A))$
35	33 34	psseq12d	$⊢ y = J (A) \to (F (suc y) \subset F (y) \leftrightarrow F (suc J (A)) \subset F (J (A)))$
36	35 4	elrab2	$⊢ J (A) \in S \leftrightarrow (J (A) \in ω \land F (suc J (A)) \subset F (J (A)))$
37	36	simprbi	$⊢ J (A) \in S \to F (suc J (A)) \subset F (J (A))$
38	20 37	syl	$⊢ (φ \land A \in ω) \to F (suc J (A)) \subset F (J (A))$
39		df-pss	$⊢ F (suc J (A)) \subset F (J (A)) \leftrightarrow (F (suc J (A)) \subseteq F (J (A)) \land F (suc J (A)) \neq F (J (A)))$
40	38 39	sylib	$⊢ (φ \land A \in ω) \to (F (suc J (A)) \subseteq F (J (A)) \land F (suc J (A)) \neq F (J (A)))$
41		pssdifn0	$⊢ (F (suc J (A)) \subseteq F (J (A)) \land F (suc J (A)) \neq F (J (A))) \to F (J (A)) ∖ F (suc J (A)) \neq \emptyset$
42	40 41	syl	$⊢ (φ \land A \in ω) \to F (J (A)) ∖ F (suc J (A)) \neq \emptyset$
43	31 42	eqnetrd	$⊢ (φ \land A \in ω) \to K (A) \neq \emptyset$

Metamath Proof Explorer

Theorem isf32lem6

Proof