isf32lem4

Description: Lemma for isfin3-2 . Being a chain, difference sets are disjoint. (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	isf32lem4	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \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		simplrr	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land A \in B) \to B \in ω$
5		simplrl	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land A \in B) \to A \in ω$
6		simpr	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land A \in B) \to A \in B$
7		simplll	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land A \in B) \to φ$
8		incom	$⊢ (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = (F (B) ∖ F (suc B)) \cap (F (A) ∖ F (suc A))$
9	1 2 3	isf32lem3	$⊢ ((B \in ω \land A \in ω) \land (A \in B \land φ)) \to (F (B) ∖ F (suc B)) \cap (F (A) ∖ F (suc A)) = \emptyset$
10	8 9	eqtrid	$⊢ ((B \in ω \land A \in ω) \land (A \in B \land φ)) \to (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \emptyset$
11	4 5 6 7 10	syl22anc	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land A \in B) \to (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \emptyset$
12		simplrl	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land B \in A) \to A \in ω$
13		simplrr	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land B \in A) \to B \in ω$
14		simpr	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land B \in A) \to B \in A$
15		simplll	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land B \in A) \to φ$
16	1 2 3	isf32lem3	$⊢ ((A \in ω \land B \in ω) \land (B \in A \land φ)) \to (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \emptyset$
17	12 13 14 15 16	syl22anc	$⊢ (((φ \land A \neq B) \land (A \in ω \land B \in ω)) \land B \in A) \to (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \emptyset$
18		simplr	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to A \neq B$
19		nnord	$⊢ A \in ω \to Ord A$
20		nnord	$⊢ B \in ω \to Ord B$
21		ordtri3	$⊢ (Ord A \land Ord B) \to (A = B \leftrightarrow \neg (A \in B \lor B \in A))$
22	19 20 21	syl2an	$⊢ (A \in ω \land B \in ω) \to (A = B \leftrightarrow \neg (A \in B \lor B \in A))$
23	22	adantl	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (A = B \leftrightarrow \neg (A \in B \lor B \in A))$
24	23	necon2abid	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to ((A \in B \lor B \in A) \leftrightarrow A \neq B)$
25	18 24	mpbird	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (A \in B \lor B \in A)$
26	11 17 25	mpjaodan	$⊢ ((φ \land A \neq B) \land (A \in ω \land B \in ω)) \to (F (A) ∖ F (suc A)) \cap (F (B) ∖ F (suc B)) = \emptyset$

Metamath Proof Explorer

Theorem isf32lem4

Proof