isf32lem3

Description: Lemma for isfin3-2 . Being a chain, difference sets are disjoint (one case). (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	isf32lem3	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \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		eldifi	$⊢ a \in (F (A) ∖ F (suc A)) \to a \in F (A)$
5		simpll	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to A \in ω$
6		peano2	$⊢ B \in ω \to suc B \in ω$
7	6	ad2antlr	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to suc B \in ω$
8		nnord	$⊢ A \in ω \to Ord A$
9	8	ad2antrr	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to Ord A$
10		simprl	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to B \in A$
11		ordsucss	$⊢ Ord A \to (B \in A \to suc B \subseteq A)$
12	9 10 11	sylc	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to suc B \subseteq A$
13		simprr	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to φ$
14	1 2 3	isf32lem1	$⊢ ((A \in ω \land suc B \in ω) \land (suc B \subseteq A \land φ)) \to F (A) \subseteq F (suc B)$
15	5 7 12 13 14	syl22anc	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to F (A) \subseteq F (suc B)$
16	15	sseld	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to (a \in F (A) \to a \in F (suc B))$
17		elndif	$⊢ a \in F (suc B) \to \neg a \in (F (B) ∖ F (suc B))$
18	4 16 17	syl56	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to (a \in (F (A) ∖ F (suc A)) \to \neg a \in (F (B) ∖ F (suc B)))$
19	18	ralrimiv	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to \forall a \in (F (A) ∖ F (suc A)) \neg a \in (F (B) ∖ F (suc B))$
20		disj	$⊢ (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \emptyset \leftrightarrow \forall a \in (F (A) ∖ F (suc A)) \neg a \in (F (B) ∖ F (suc B))$
21	19 20	sylibr	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \emptyset$

Metamath Proof Explorer

Theorem isf32lem3

Proof