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 syl5eq ( ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) ∧ ( 𝐴𝐵𝜑 ) ) → ( ( ( 𝐹𝐴 ) ∖ ( 𝐹 ‘ 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 𝐵 ) ) ) = ∅ )