Metamath Proof Explorer

Theorem ltsintdifex

Description: If A , then the intersection of all the ordinals that have differing signs in A and B exists. (Contributed by Scott Fenton, 22-Feb-2012)

Ref Expression
Assertion ltsintdifex ⊢ A ∈ No ∧ B ∈ No → A < s B → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V

Proof

Step Hyp Ref Expression
1 ltsval2 ⊢ A ∈ No ∧ B ∈ No → A < s B ↔ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a
2 fvex ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
3 fvex ⊢ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
4 2 3 brtp ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ↔ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ ∨ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 ∨ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜
5 fvprc ⊢ ¬ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V → A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅
6 1n0 ⊢ 1 𝑜 ≠ ∅
7 6 neii ⊢ ¬ 1 𝑜 = ∅
8 eqeq1 ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ → A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ↔ ∅ = 1 𝑜
9 eqcom ⊢ ∅ = 1 𝑜 ↔ 1 𝑜 = ∅
10 8 9 bitrdi ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ → A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ↔ 1 𝑜 = ∅
11 7 10 mtbiri ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ → ¬ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜
12 5 11 syl ⊢ ¬ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V → ¬ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜
13 12 con4i ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
14 13 adantr ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
15 13 adantr ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
16 fvprc ⊢ ¬ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V → B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅
17 2on0 ⊢ 2 𝑜 ≠ ∅
18 17 neii ⊢ ¬ 2 𝑜 = ∅
19 eqeq1 ⊢ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ → B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 ↔ ∅ = 2 𝑜
20 eqcom ⊢ ∅ = 2 𝑜 ↔ 2 𝑜 = ∅
21 19 20 bitrdi ⊢ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ → B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 ↔ 2 𝑜 = ∅
22 18 21 mtbiri ⊢ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ → ¬ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜
23 16 22 syl ⊢ ¬ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V → ¬ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜
24 23 con4i ⊢ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
25 24 adantl ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
26 14 15 25 3jaoi ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ ∨ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 1 𝑜 ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 ∨ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = ∅ ∧ B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a = 2 𝑜 → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
27 4 26 sylbi ⊢ A ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a 1 𝑜 ∅ 1 𝑜 2 𝑜 ∅ 2 𝑜 B ⁡ ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V
28 1 27 biimtrdi ⊢ A ∈ No ∧ B ∈ No → A < s B → ⋂ a ∈ On | A ⁡ a ≠ B ⁡ a ∈ V