This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
Assertion isf32lem3 ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ )

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
2 isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
3 isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
4 eldifi ⊢ ( 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) → 𝑎 ∈ ( 𝐹 ‘ 𝐴 ) )
5 simpll ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → 𝐴 ∈ ω )
6 peano2 ⊢ ( 𝐵 ∈ ω → suc 𝐵 ∈ ω )
7 6 ad2antlr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → suc 𝐵 ∈ ω )
8 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
9 8 ad2antrr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → Ord 𝐴 )
10 simprl ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → 𝐵 ∈ 𝐴 )
11 ordsucss ⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
12 9 10 11 sylc ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → suc 𝐵 ⊆ 𝐴 )
13 simprr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → 𝜑 )
14 1 2 3 isf32lem1 ⊢ ( ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ ( suc 𝐵 ⊆ 𝐴 ∧ 𝜑 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐵 ) )
15 5 7 12 13 14 syl22anc ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝐹 ‘ 𝐴 ) ⊆ ( 𝐹 ‘ suc 𝐵 ) )
16 15 sseld ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝑎 ∈ ( 𝐹 ‘ 𝐴 ) → 𝑎 ∈ ( 𝐹 ‘ suc 𝐵 ) ) )
17 elndif ⊢ ( 𝑎 ∈ ( 𝐹 ‘ suc 𝐵 ) → ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) )
18 4 16 17 syl56 ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) → ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) )
19 18 ralrimiv ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ∀ 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) )
20 disj ⊢ ( ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ ↔ ∀ 𝑎 ∈ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ¬ 𝑎 ∈ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) )
21 19 20 sylibr ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ )