Metamath Proof Explorer

Theorem sltintdifex

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 sltintdifex ⊢A∈No∧B∈No→A<sB→⋂a∈On|A⁡a≠B⁡a∈V

Proof

Step Hyp Ref Expression
1 sltval2 ⊢A∈No∧B∈No→A<sB↔A⁡⋂a∈On|A⁡a≠B⁡a1𝑜∅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⁡a1𝑜∅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⁡a1𝑜∅1𝑜2𝑜∅2𝑜B⁡⋂a∈On|A⁡a≠B⁡a→⋂a∈On|A⁡a≠B⁡a∈V
28 1 27 syl6bi ⊢A∈No∧B∈No→A<sB→⋂a∈On|A⁡a≠B⁡a∈V