isf32lem1

Description: Lemma for isfin3-2 . Derive weak ordering property. (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$
Assertion	isf32lem1	$⊢ ((A \in ω \land B \in ω) \land (B \subseteq A \land φ)) \to F (A) \subseteq F (B)$

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		fveq2	$⊢ a = B \to F (a) = F (B)$
5	4	sseq1d	$⊢ a = B \to (F (a) \subseteq F (B) \leftrightarrow F (B) \subseteq F (B))$
6	5	imbi2d	$⊢ a = B \to ((φ \to F (a) \subseteq F (B)) \leftrightarrow (φ \to F (B) \subseteq F (B)))$
7		fveq2	$⊢ a = b \to F (a) = F (b)$
8	7	sseq1d	$⊢ a = b \to (F (a) \subseteq F (B) \leftrightarrow F (b) \subseteq F (B))$
9	8	imbi2d	$⊢ a = b \to ((φ \to F (a) \subseteq F (B)) \leftrightarrow (φ \to F (b) \subseteq F (B)))$
10		fveq2	$⊢ a = suc b \to F (a) = F (suc b)$
11	10	sseq1d	$⊢ a = suc b \to (F (a) \subseteq F (B) \leftrightarrow F (suc b) \subseteq F (B))$
12	11	imbi2d	$⊢ a = suc b \to ((φ \to F (a) \subseteq F (B)) \leftrightarrow (φ \to F (suc b) \subseteq F (B)))$
13		fveq2	$⊢ a = A \to F (a) = F (A)$
14	13	sseq1d	$⊢ a = A \to (F (a) \subseteq F (B) \leftrightarrow F (A) \subseteq F (B))$
15	14	imbi2d	$⊢ a = A \to ((φ \to F (a) \subseteq F (B)) \leftrightarrow (φ \to F (A) \subseteq F (B)))$
16		ssid	$⊢ F (B) \subseteq F (B)$
17	16	2a1i	$⊢ B \in ω \to (φ \to F (B) \subseteq F (B))$
18		suceq	$⊢ x = b \to suc x = suc b$
19	18	fveq2d	$⊢ x = b \to F (suc x) = F (suc b)$
20		fveq2	$⊢ x = b \to F (x) = F (b)$
21	19 20	sseq12d	$⊢ x = b \to (F (suc x) \subseteq F (x) \leftrightarrow F (suc b) \subseteq F (b))$
22	21	rspcv	$⊢ b \in ω \to (\forall x \in ω F (suc x) \subseteq F (x) \to F (suc b) \subseteq F (b))$
23	2 22	syl5	$⊢ b \in ω \to (φ \to F (suc b) \subseteq F (b))$
24	23	ad2antrr	$⊢ ((b \in ω \land B \in ω) \land B \subseteq b) \to (φ \to F (suc b) \subseteq F (b))$
25		sstr2	$⊢ F (suc b) \subseteq F (b) \to (F (b) \subseteq F (B) \to F (suc b) \subseteq F (B))$
26	24 25	syl6	$⊢ ((b \in ω \land B \in ω) \land B \subseteq b) \to (φ \to (F (b) \subseteq F (B) \to F (suc b) \subseteq F (B)))$
27	26	a2d	$⊢ ((b \in ω \land B \in ω) \land B \subseteq b) \to ((φ \to F (b) \subseteq F (B)) \to (φ \to F (suc b) \subseteq F (B)))$
28	6 9 12 15 17 27	findsg	$⊢ ((A \in ω \land B \in ω) \land B \subseteq A) \to (φ \to F (A) \subseteq F (B))$
29	28	impr	$⊢ ((A \in ω \land B \in ω) \land (B \subseteq A \land φ)) \to F (A) \subseteq F (B)$

Metamath Proof Explorer

Theorem isf32lem1

Proof