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 e. No /\ B e. No ) -> ( A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V ) )

Proof

Step Hyp Ref Expression
1 sltval2 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) ) )
2 fvex 
 |-  ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
3 fvex 
 |-  ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) e. _V
4 2 3 brtp 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) <-> ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) )
5 fvprc 
 |-  ( -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V -> ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
6 1n0 
 |-  1o =/= (/)
7 6 neii 
 |-  -. 1o = (/)
8 eqeq1 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o <-> (/) = 1o ) )
9 eqcom 
 |-  ( (/) = 1o <-> 1o = (/) )
10 8 9 bitrdi 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o <-> 1o = (/) ) )
11 7 10 mtbiri 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> -. ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o )
12 5 11 syl 
 |-  ( -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V -> -. ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o )
13 12 con4i 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
14 13 adantr 
 |-  ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
15 13 adantr 
 |-  ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
16 fvprc 
 |-  ( -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V -> ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) )
17 2on0 
 |-  2o =/= (/)
18 17 neii 
 |-  -. 2o = (/)
19 eqeq1 
 |-  ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o <-> (/) = 2o ) )
20 eqcom 
 |-  ( (/) = 2o <-> 2o = (/) )
21 19 20 bitrdi 
 |-  ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o <-> 2o = (/) ) )
22 18 21 mtbiri 
 |-  ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o )
23 16 22 syl 
 |-  ( -. |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V -> -. ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o )
24 23 con4i 
 |-  ( ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
25 24 adantl 
 |-  ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
26 14 15 25 3jaoi 
 |-  ( ( ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 1o /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) \/ ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = (/) /\ ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) = 2o ) ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
27 4 26 sylbi 
 |-  ( ( A ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { a e. On | ( A ` a ) =/= ( B ` a ) } ) -> |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V )
28 1 27 syl6bi 
 |-  ( ( A e. No /\ B e. No ) -> ( A  |^| { a e. On | ( A ` a ) =/= ( B ` a ) } e. _V ) )