isf32lem8

Description: Lemma for isfin3-2 . K sets are subsets of the base. (Contributed by Stefan O'Rear, 6-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	isf32lem8	$⊢ (φ \land A \in ω) \to K (A) \subseteq G$

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	13	ffvelrnda	$⊢ (φ \land A \in ω) \to J (A) \in S$
17		fveq2	$⊢ w = J (A) \to F (w) = F (J (A))$
18		suceq	$⊢ w = J (A) \to suc w = suc J (A)$
19	18	fveq2d	$⊢ w = J (A) \to F (suc w) = F (suc J (A))$
20	17 19	difeq12d	$⊢ w = J (A) \to F (w) ∖ F (suc w) = F (J (A)) ∖ F (suc J (A))$
21		eqid	$⊢ (w \in S ⟼ F (w) ∖ F (suc w)) = (w \in S ⟼ F (w) ∖ F (suc w))$
22		fvex	$⊢ F (J (A)) \in V$
23	22	difexi	$⊢ F (J (A)) ∖ F (suc J (A)) \in V$
24	20 21 23	fvmpt	$⊢ J (A) \in S \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (A)) = F (J (A)) ∖ F (suc J (A))$
25	16 24	syl	$⊢ (φ \land A \in ω) \to (w \in S ⟼ F (w) ∖ F (suc w)) (J (A)) = F (J (A)) ∖ F (suc J (A))$
26	15 25	eqtrd	$⊢ (φ \land A \in ω) \to ((w \in S ⟼ F (w) ∖ F (suc w)) \circ J) (A) = F (J (A)) ∖ F (suc J (A))$
27	7 26	syl5eq	$⊢ (φ \land A \in ω) \to K (A) = F (J (A)) ∖ F (suc J (A))$
28	1	adantr	$⊢ (φ \land A \in ω) \to F : ω ⟶ 𝒫 G$
29	8 16	sseldi	$⊢ (φ \land A \in ω) \to J (A) \in ω$
30	28 29	ffvelrnd	$⊢ (φ \land A \in ω) \to F (J (A)) \in 𝒫 G$
31	30	elpwid	$⊢ (φ \land A \in ω) \to F (J (A)) \subseteq G$
32	31	ssdifssd	$⊢ (φ \land A \in ω) \to F (J (A)) ∖ F (suc J (A)) \subseteq G$
33	27 32	eqsstrd	$⊢ (φ \land A \in ω) \to K (A) \subseteq G$

Metamath Proof Explorer

Theorem isf32lem8

Proof