Metamath Proof Explorer

Theorem nosepdmlem

Description: Lemma for nosepdm . (Contributed by Scott Fenton, 24-Nov-2021)

Ref Expression
Assertion nosepdmlem 
|- ( ( A e. No /\ B e. No /\ A  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) )

Proof

Step Hyp Ref Expression
1 sltval2 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
2 fvex 
 |-  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) e. _V
3 fvex 
 |-  ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) e. _V
4 2 3 brtp 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) <-> ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
5 df-3or 
 |-  ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) <-> ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
6 ndmfv 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
7 1oex 
 |-  1o e. _V
8 7 prid1 
 |-  1o e. { 1o , 2o }
9 8 nosgnn0i 
 |-  (/) =/= 1o
10 neeq1 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= 1o <-> (/) =/= 1o ) )
11 9 10 mpbiri 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= 1o )
12 11 neneqd 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> -. ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o )
13 12 intnanrd 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> -. ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) )
14 12 intnanrd 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> -. ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) )
15 ioran 
 |-  ( -. ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) <-> ( -. ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) /\ -. ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
16 13 14 15 sylanbrc 
 |-  ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> -. ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
17 6 16 syl 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> -. ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
18 17 adantl 
 |-  ( ( ( A e. No /\ B e. No ) /\ -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) -> -. ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
19 orel1 
 |-  ( -. ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> ( ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
20 18 19 syl 
 |-  ( ( ( A e. No /\ B e. No ) /\ -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) -> ( ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
21 5 20 syl5bi 
 |-  ( ( ( A e. No /\ B e. No ) /\ -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) -> ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) )
22 ndmfv 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
23 2on 
 |-  2o e. On
24 23 elexi 
 |-  2o e. _V
25 24 prid2 
 |-  2o e. { 1o , 2o }
26 25 nosgnn0i 
 |-  (/) =/= 2o
27 neeq1 
 |-  ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= 2o <-> (/) =/= 2o ) )
28 26 27 mpbiri 
 |-  ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= 2o )
29 22 28 syl 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= 2o )
30 29 neneqd 
 |-  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B -> -. ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o )
31 30 con4i 
 |-  ( ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B )
32 31 adantl 
 |-  ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B )
33 21 32 syl6 
 |-  ( ( ( A e. No /\ B e. No ) /\ -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A ) -> ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) )
34 33 ex 
 |-  ( ( A e. No /\ B e. No ) -> ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) ) )
35 34 com23 
 |-  ( ( A e. No /\ B e. No ) -> ( ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) \/ ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) ) -> ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) ) )
36 4 35 syl5bi 
 |-  ( ( A e. No /\ B e. No ) -> ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) -> ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) ) )
37 1 36 sylbid 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) ) )
38 37 3impia 
 |-  ( ( A e. No /\ B e. No /\ A  ( -. |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A -> |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) )
39 38 orrd 
 |-  ( ( A e. No /\ B e. No /\ A  ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A \/ |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) )
40 elun 
 |-  ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) <-> ( |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom A \/ |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. dom B ) )
41 39 40 sylibr 
 |-  ( ( A e. No /\ B e. No /\ A  |^| { x e. On | ( A ` x ) =/= ( B ` x ) } e. ( dom A u. dom B ) )