Metamath Proof Explorer

Theorem nolesgn2o

Description: Given A less than or equal to B , equal to B up to X , and A ( X ) = 2o , then B ( X ) = 2o . (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Assertion nolesgn2o 
|- ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ -. B  ( B ` X ) = 2o )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> B e. No )
2 nofv 
 |-  ( B e. No -> ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) )
3 1 2 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) )
4 3orel3 
 |-  ( -. ( B ` X ) = 2o -> ( ( ( B ` X ) = (/) \/ ( B ` X ) = 1o \/ ( B ` X ) = 2o ) -> ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) )
5 3 4 syl5com 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( -. ( B ` X ) = 2o -> ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) )
6 simp13 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> X e. On )
7 fveq1 
 |-  ( ( A |` X ) = ( B |` X ) -> ( ( A |` X ) ` y ) = ( ( B |` X ) ` y ) )
8 7 eqcomd 
 |-  ( ( A |` X ) = ( B |` X ) -> ( ( B |` X ) ` y ) = ( ( A |` X ) ` y ) )
9 8 adantr 
 |-  ( ( ( A |` X ) = ( B |` X ) /\ y e. X ) -> ( ( B |` X ) ` y ) = ( ( A |` X ) ` y ) )
10 simpr 
 |-  ( ( ( A |` X ) = ( B |` X ) /\ y e. X ) -> y e. X )
11 10 fvresd 
 |-  ( ( ( A |` X ) = ( B |` X ) /\ y e. X ) -> ( ( B |` X ) ` y ) = ( B ` y ) )
12 10 fvresd 
 |-  ( ( ( A |` X ) = ( B |` X ) /\ y e. X ) -> ( ( A |` X ) ` y ) = ( A ` y ) )
13 9 11 12 3eqtr3d 
 |-  ( ( ( A |` X ) = ( B |` X ) /\ y e. X ) -> ( B ` y ) = ( A ` y ) )
14 13 ralrimiva 
 |-  ( ( A |` X ) = ( B |` X ) -> A. y e. X ( B ` y ) = ( A ` y ) )
15 14 adantr 
 |-  ( ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) -> A. y e. X ( B ` y ) = ( A ` y ) )
16 15 3ad2ant2 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> A. y e. X ( B ` y ) = ( A ` y ) )
17 simprr 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( A ` X ) = 2o )
18 17 a1d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( ( B ` X ) = (/) -> ( A ` X ) = 2o ) )
19 18 ancld 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( ( B ` X ) = (/) -> ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) ) )
20 17 a1d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( ( B ` X ) = 1o -> ( A ` X ) = 2o ) )
21 20 ancld 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( ( B ` X ) = 1o -> ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) ) )
22 19 21 orim12d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) -> ( ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) ) ) )
23 22 3impia 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> ( ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) ) )
24 3mix3 
 |-  ( ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) -> ( ( ( B ` X ) = 1o /\ ( A ` X ) = (/) ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) ) )
25 3mix2 
 |-  ( ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) -> ( ( ( B ` X ) = 1o /\ ( A ` X ) = (/) ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) ) )
26 24 25 jaoi 
 |-  ( ( ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) ) -> ( ( ( B ` X ) = 1o /\ ( A ` X ) = (/) ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) ) )
27 23 26 syl 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> ( ( ( B ` X ) = 1o /\ ( A ` X ) = (/) ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) ) )
28 fvex 
 |-  ( B ` X ) e. _V
29 fvex 
 |-  ( A ` X ) e. _V
30 28 29 brtp 
 |-  ( ( B ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` X ) <-> ( ( ( B ` X ) = 1o /\ ( A ` X ) = (/) ) \/ ( ( B ` X ) = 1o /\ ( A ` X ) = 2o ) \/ ( ( B ` X ) = (/) /\ ( A ` X ) = 2o ) ) )
31 27 30 sylibr 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> ( B ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` X ) )
32 raleq 
 |-  ( x = X -> ( A. y e. x ( B ` y ) = ( A ` y ) <-> A. y e. X ( B ` y ) = ( A ` y ) ) )
33 fveq2 
 |-  ( x = X -> ( B ` x ) = ( B ` X ) )
34 fveq2 
 |-  ( x = X -> ( A ` x ) = ( A ` X ) )
35 33 34 breq12d 
 |-  ( x = X -> ( ( B ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` x ) <-> ( B ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` X ) ) )
36 32 35 anbi12d 
 |-  ( x = X -> ( ( A. y e. x ( B ` y ) = ( A ` y ) /\ ( B ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` x ) ) <-> ( A. y e. X ( B ` y ) = ( A ` y ) /\ ( B ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` X ) ) ) )
37 36 rspcev 
 |-  ( ( X e. On /\ ( A. y e. X ( B ` y ) = ( A ` y ) /\ ( B ` X ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` X ) ) ) -> E. x e. On ( A. y e. x ( B ` y ) = ( A ` y ) /\ ( B ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` x ) ) )
38 6 16 31 37 syl12anc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> E. x e. On ( A. y e. x ( B ` y ) = ( A ` y ) /\ ( B ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` x ) ) )
39 simp12 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> B e. No )
40 simp11 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> A e. No )
41 sltval 
 |-  ( ( B e. No /\ A e. No ) -> ( B  E. x e. On ( A. y e. x ( B ` y ) = ( A ` y ) /\ ( B ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` x ) ) ) )
42 39 40 41 syl2anc 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> ( B  E. x e. On ( A. y e. x ( B ` y ) = ( A ` y ) /\ ( B ` x ) { <. 1o , (/) >. , <. 1o , 2o >. , <. (/) , 2o >. } ( A ` x ) ) ) )
43 38 42 mpbird 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) ) -> B
44 43 3expia 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( ( ( B ` X ) = (/) \/ ( B ` X ) = 1o ) -> B
45 5 44 syld 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( -. ( B ` X ) = 2o -> B
46 45 con1d 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) ) -> ( -. B  ( B ` X ) = 2o ) )
47 46 3impia 
 |-  ( ( ( A e. No /\ B e. No /\ X e. On ) /\ ( ( A |` X ) = ( B |` X ) /\ ( A ` X ) = 2o ) /\ -. B  ( B ` X ) = 2o )