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 < s B a On | A a B a V

Proof

Step Hyp Ref Expression
1 sltval2 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 syl6bi A No B No A < s B a On | A a B a V