Metamath Proof Explorer

Theorem nogesgn1o

Description: Given A greater than or equal to B , equal to B up to X , and A ( X ) = 1o , then B ( X ) = 1o . (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

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