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

Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 isf32lem.a ⊢ ( 𝜑 → 𝐹 : ω ⟶ 𝒫 𝐺 )
2 isf32lem.b ⊢ ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹 ‘ 𝑥 ) )
3 isf32lem.c ⊢ ( 𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹 )
4 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝐵 ∈ ω )
5 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ω )
6 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ 𝐵 )
7 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐴 ∈ 𝐵 ) → 𝜑 )
8 incom ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ( ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ∩ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) )
9 1 2 3 isf32lem3 ⊢ ( ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝜑 ) ) → ( ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ∩ ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ) = ∅ )
10 8 9 eqtrid ⊢ ( ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ∧ ( 𝐴 ∈ 𝐵 ∧ 𝜑 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ )
11 4 5 6 7 10 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐴 ∈ 𝐵 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ )
12 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ∈ ω )
13 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ω )
14 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ 𝐴 )
15 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐵 ∈ 𝐴 ) → 𝜑 )
16 1 2 3 isf32lem3 ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ∧ ( 𝐵 ∈ 𝐴 ∧ 𝜑 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ )
17 12 13 14 15 16 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) ∧ 𝐵 ∈ 𝐴 ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ )
18 simplr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → 𝐴 ≠ 𝐵 )
19 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
20 nnord ⊢ ( 𝐵 ∈ ω → Ord 𝐵 )
21 ordtri3 ⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
22 19 20 21 syl2an ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 = 𝐵 ↔ ¬ ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ) )
24 23 necon2abid ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) ↔ 𝐴 ≠ 𝐵 ) )
25 18 24 mpbird ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 ∨ 𝐵 ∈ 𝐴 ) )
26 11 17 25 mpjaodan ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ( ( 𝐹 ‘ 𝐴 ) ∖ ( 𝐹 ‘ suc 𝐴 ) ) ∩ ( ( 𝐹 ‘ 𝐵 ) ∖ ( 𝐹 ‘ suc 𝐵 ) ) ) = ∅ )