Metamath Proof Explorer

Theorem 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 ⊢ φ → F : ω ⟶ 𝒫 G
isf32lem.b ⊢ φ → ∀ x ∈ ω F ⁡ suc ⁡ x ⊆ F ⁡ x
isf32lem.c ⊢ φ → ¬ ⋂ ran ⁡ F ∈ ran ⁡ F
Assertion isf32lem3 ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → F ⁡ A ∖ F ⁡ suc ⁡ A ∩ F ⁡ B ∖ F ⁡ suc ⁡ B = ∅

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ φ → F : ω ⟶ 𝒫 G
2 isf32lem.b ⊢ φ → ∀ x ∈ ω F ⁡ suc ⁡ x ⊆ F ⁡ x
3 isf32lem.c ⊢ φ → ¬ ⋂ ran ⁡ F ∈ ran ⁡ F
4 eldifi ⊢ a ∈ F ⁡ A ∖ F ⁡ suc ⁡ A → a ∈ F ⁡ A
5 simpll ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → A ∈ ω
6 peano2 ⊢ B ∈ ω → suc ⁡ B ∈ ω
7 6 ad2antlr ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → suc ⁡ B ∈ ω
8 nnord ⊢ A ∈ ω → Ord ⁡ A
9 8 ad2antrr ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → Ord ⁡ A
10 simprl ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → B ∈ A
11 ordsucss ⊢ Ord ⁡ A → B ∈ A → suc ⁡ B ⊆ A
12 9 10 11 sylc ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → suc ⁡ B ⊆ A
13 simprr ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → φ
14 1 2 3 isf32lem1 ⊢ A ∈ ω ∧ suc ⁡ B ∈ ω ∧ suc ⁡ B ⊆ A ∧ φ → F ⁡ A ⊆ F ⁡ suc ⁡ B
15 5 7 12 13 14 syl22anc ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → F ⁡ A ⊆ F ⁡ suc ⁡ B
16 15 sseld ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → a ∈ F ⁡ A → a ∈ F ⁡ suc ⁡ B
17 elndif ⊢ a ∈ F ⁡ suc ⁡ B → ¬ a ∈ F ⁡ B ∖ F ⁡ suc ⁡ B
18 4 16 17 syl56 ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → a ∈ F ⁡ A ∖ F ⁡ suc ⁡ A → ¬ a ∈ F ⁡ B ∖ F ⁡ suc ⁡ B
19 18 ralrimiv ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → ∀ a ∈ F ⁡ A ∖ F ⁡ suc ⁡ A ¬ a ∈ F ⁡ B ∖ F ⁡ suc ⁡ B
20 disj ⊢ F ⁡ A ∖ F ⁡ suc ⁡ A ∩ F ⁡ B ∖ F ⁡ suc ⁡ B = ∅ ↔ ∀ a ∈ F ⁡ A ∖ F ⁡ suc ⁡ A ¬ a ∈ F ⁡ B ∖ F ⁡ suc ⁡ B
21 19 20 sylibr ⊢ A ∈ ω ∧ B ∈ ω ∧ B ∈ A ∧ φ → F ⁡ A ∖ F ⁡ suc ⁡ A ∩ F ⁡ B ∖ F ⁡ suc ⁡ B = ∅