Metamath Proof Explorer

Theorem dyaddisj

Description: Two closed dyadic rational intervals are either in a subset relationship or are almost disjoint (the interiors are disjoint). (Contributed by Mario Carneiro, 26-Mar-2015)

Ref Expression
Hypothesis dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
Assertion dyaddisj ( ( 𝐴 ∈ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) → ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ∨ ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ∨ ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 dyadmbl.1 ⊢ 𝐹 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℕ0 ↦ ⟨ ( 𝑥 / ( 2 ↑ 𝑦 ) ) , ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑦 ) ) ⟩ )
2 1 dyadf ⊢ 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) )
3 ffn ⊢ ( 𝐹 : ( ℤ × ℕ0 ) ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) → 𝐹 Fn ( ℤ × ℕ0 ) )
4 ovelrn ⊢ ( 𝐹 Fn ( ℤ × ℕ0 ) → ( 𝐴 ∈ ran 𝐹 ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ) )
5 ovelrn ⊢ ( 𝐹 Fn ( ℤ × ℕ0 ) → ( 𝐵 ∈ ran 𝐹 ↔ ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) )
6 4 5 anbi12d ⊢ ( 𝐹 Fn ( ℤ × ℕ0 ) → ( ( 𝐴 ∈ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) ↔ ( ∃ 𝑎 ∈ ℤ ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) ) )
7 2 3 6 mp2b ⊢ ( ( 𝐴 ∈ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) ↔ ( ∃ 𝑎 ∈ ℤ ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) )
8 reeanv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) ↔ ( ∃ 𝑎 ∈ ℤ ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑏 ∈ ℤ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) )
9 7 8 bitr4i ⊢ ( ( 𝐴 ∈ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) )
10 reeanv ⊢ ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℕ0 ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) ↔ ( ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) )
11 nn0re ⊢ ( 𝑐 ∈ ℕ0 → 𝑐 ∈ ℝ )
12 11 ad2antrl ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) → 𝑐 ∈ ℝ )
13 nn0re ⊢ ( 𝑑 ∈ ℕ0 → 𝑑 ∈ ℝ )
14 13 ad2antll ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) → 𝑑 ∈ ℝ )
15 1 dyaddisjlem ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) ∧ 𝑐 ≤ 𝑑 ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) )
16 ancom ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ↔ ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) )
17 ancom ⊢ ( ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ↔ ( 𝑑 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) )
18 16 17 anbi12i ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) ↔ ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ) )
19 1 dyaddisjlem ⊢ ( ( ( ( 𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑑 ∈ ℕ0 ∧ 𝑐 ∈ ℕ0 ) ) ∧ 𝑑 ≤ 𝑐 ) → ( ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ∅ ) )
20 18 19 sylanb ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) ∧ 𝑑 ≤ 𝑐 ) → ( ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ∅ ) )
21 orcom ⊢ ( ( ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ↔ ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ) )
22 incom ⊢ ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) )
23 22 eqeq1i ⊢ ( ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ∅ ↔ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ )
24 21 23 orbi12i ⊢ ( ( ( ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ∨ ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ∅ ) ↔ ( ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) )
25 df-3or ⊢ ( ( ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ∅ ) ↔ ( ( ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) ∨ ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ∅ ) )
26 df-3or ⊢ ( ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) ↔ ( ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) )
27 24 25 26 3bitr4i ⊢ ( ( ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ∩ ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ) = ∅ ) ↔ ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) )
28 20 27 sylib ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) ∧ 𝑑 ≤ 𝑐 ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) )
29 12 14 15 28 lecasei ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) → ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) )
30 simpl ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → 𝐴 = ( 𝑎 𝐹 𝑐 ) )
31 30 fveq2d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( [,] ‘ 𝐴 ) = ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) )
32 simpr ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → 𝐵 = ( 𝑏 𝐹 𝑑 ) )
33 32 fveq2d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( [,] ‘ 𝐵 ) = ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) )
34 31 33 sseq12d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ↔ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ) )
35 33 31 sseq12d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ↔ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ) )
36 30 fveq2d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( (,) ‘ 𝐴 ) = ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) )
37 32 fveq2d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( (,) ‘ 𝐵 ) = ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) )
38 36 37 ineq12d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) )
39 38 eqeq1d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ↔ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) )
40 34 35 39 3orbi123d ⊢ ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ∨ ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ∨ ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ) ↔ ( ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ⊆ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ∨ ( [,] ‘ ( 𝑏 𝐹 𝑑 ) ) ⊆ ( [,] ‘ ( 𝑎 𝐹 𝑐 ) ) ∨ ( ( (,) ‘ ( 𝑎 𝐹 𝑐 ) ) ∩ ( (,) ‘ ( 𝑏 𝐹 𝑑 ) ) ) = ∅ ) ) )
41 29 40 syl5ibrcom ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ ( 𝑐 ∈ ℕ0 ∧ 𝑑 ∈ ℕ0 ) ) → ( ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ∨ ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ∨ ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ) ) )
42 41 rexlimdvva ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ∃ 𝑐 ∈ ℕ0 ∃ 𝑑 ∈ ℕ0 ( 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ∨ ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ∨ ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ) ) )
43 10 42 biimtrrid ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ∨ ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ∨ ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ) ) )
44 43 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ∃ 𝑐 ∈ ℕ0 𝐴 = ( 𝑎 𝐹 𝑐 ) ∧ ∃ 𝑑 ∈ ℕ0 𝐵 = ( 𝑏 𝐹 𝑑 ) ) → ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ∨ ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ∨ ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ) )
45 9 44 sylbi ⊢ ( ( 𝐴 ∈ ran 𝐹 ∧ 𝐵 ∈ ran 𝐹 ) → ( ( [,] ‘ 𝐴 ) ⊆ ( [,] ‘ 𝐵 ) ∨ ( [,] ‘ 𝐵 ) ⊆ ( [,] ‘ 𝐴 ) ∨ ( ( (,) ‘ 𝐴 ) ∩ ( (,) ‘ 𝐵 ) ) = ∅ ) )