Metamath Proof Explorer

Theorem nosepnelem

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

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

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 1n0 
 |-  1o =/= (/)
6 simpl 
 |-  ( ( ( 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 )
7 simpr 
 |-  ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) ) -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) )
8 6 7 neeq12d 
 |-  ( ( ( 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 ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) <-> 1o =/= (/) ) )
9 5 8 mpbiri 
 |-  ( ( ( 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 ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
10 df-2o 
 |-  2o = suc 1o
11 df-1o 
 |-  1o = suc (/)
12 10 11 eqeq12i 
 |-  ( 2o = 1o <-> suc 1o = suc (/) )
13 1on 
 |-  1o e. On
14 0elon 
 |-  (/) e. On
15 suc11 
 |-  ( ( 1o e. On /\ (/) e. On ) -> ( suc 1o = suc (/) <-> 1o = (/) ) )
16 13 14 15 mp2an 
 |-  ( suc 1o = suc (/) <-> 1o = (/) )
17 12 16 bitri 
 |-  ( 2o = 1o <-> 1o = (/) )
18 17 necon3bii 
 |-  ( 2o =/= 1o <-> 1o =/= (/) )
19 5 18 mpbir 
 |-  2o =/= 1o
20 19 necomi 
 |-  1o =/= 2o
21 simpl 
 |-  ( ( ( 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 )
22 simpr 
 |-  ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 1o /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o )
23 21 22 neeq12d 
 |-  ( ( ( 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 ) } ) <-> 1o =/= 2o ) )
24 20 23 mpbiri 
 |-  ( ( ( 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 ) } ) )
25 2on 
 |-  2o e. On
26 25 elexi 
 |-  2o e. _V
27 26 prid2 
 |-  2o e. { 1o , 2o }
28 27 nosgnn0i 
 |-  (/) =/= 2o
29 simpl 
 |-  ( ( ( 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 ) } ) = (/) )
30 simpr 
 |-  ( ( ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = (/) /\ ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o ) -> ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) = 2o )
31 29 30 neeq12d 
 |-  ( ( ( 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 ) )
32 28 31 mpbiri 
 |-  ( ( ( 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 ) } ) )
33 9 24 32 3jaoi 
 |-  ( ( ( ( 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 ) } ) )
34 4 33 sylbi 
 |-  ( ( 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 ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )
35 1 34 syl6bi 
 |-  ( ( A e. No /\ B e. No ) -> ( A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) ) )
36 35 3impia 
 |-  ( ( A e. No /\ B e. No /\ A  ( A ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) =/= ( B ` |^| { x e. On | ( A ` x ) =/= ( B ` x ) } ) )