Metamath Proof Explorer


Theorem nogt01o

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

Ref Expression
Assertion nogt01o A No B No X On A X = B X A < s B B X = A X = 1 𝑜

Proof

Step Hyp Ref Expression
1 sltso < s Or No
2 simp11 A No B No X On A X = B X A < s B B X = A No
3 sonr < s Or No A No ¬ A < s A
4 1 2 3 sylancr A No B No X On A X = B X A < s B B X = ¬ A < s A
5 simpl2r A No B No X On A X = B X A < s B B X = A X = A < s B
6 simpl2l A No B No X On A X = B X A < s B B X = A X = A X = B X
7 simpl11 A No B No X On A X = B X A < s B B X = A X = A No
8 nofun A No Fun A
9 funrel Fun A Rel A
10 8 9 syl A No Rel A
11 7 10 syl A No B No X On A X = B X A < s B B X = A X = Rel A
12 simpl13 A No B No X On A X = B X A < s B B X = A X = X On
13 simpr A No B No X On A X = B X A < s B B X = A X = A X =
14 nolt02olem A No X On A X = dom A X
15 7 12 13 14 syl3anc A No B No X On A X = B X A < s B B X = A X = dom A X
16 relssres Rel A dom A X A X = A
17 11 15 16 syl2anc A No B No X On A X = B X A < s B B X = A X = A X = A
18 simpl12 A No B No X On A X = B X A < s B B X = A X = B No
19 nofun B No Fun B
20 funrel Fun B Rel B
21 19 20 syl B No Rel B
22 18 21 syl A No B No X On A X = B X A < s B B X = A X = Rel B
23 simpl3 A No B No X On A X = B X A < s B B X = A X = B X =
24 nolt02olem B No X On B X = dom B X
25 18 12 23 24 syl3anc A No B No X On A X = B X A < s B B X = A X = dom B X
26 relssres Rel B dom B X B X = B
27 22 25 26 syl2anc A No B No X On A X = B X A < s B B X = A X = B X = B
28 6 17 27 3eqtr3d A No B No X On A X = B X A < s B B X = A X = A = B
29 5 28 breqtrrd A No B No X On A X = B X A < s B B X = A X = A < s A
30 4 29 mtand A No B No X On A X = B X A < s B B X = ¬ A X =
31 simp2r A No B No X On A X = B X A < s B B X = A < s B
32 simp12 A No B No X On A X = B X A < s B B X = B No
33 sltval A No B No A < s B x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
34 2 32 33 syl2anc A No B No X On A X = B X A < s B B X = A < s B x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
35 31 34 mpbid A No B No X On A X = B X A < s B B X = x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
36 ralinexa x On y x A y = B y ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x ¬ x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
37 36 con2bii x On y x A y = B y A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x ¬ x On y x A y = B y ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
38 35 37 sylib A No B No X On A X = B X A < s B B X = ¬ x On y x A y = B y ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
39 1n0 1 𝑜
40 39 neii ¬ 1 𝑜 =
41 eqtr2 A X x = 1 𝑜 A X x = 1 𝑜 =
42 40 41 mto ¬ A X x = 1 𝑜 A X x =
43 df-2o 2 𝑜 = suc 1 𝑜
44 2on 2 𝑜 On
45 43 44 eqeltrri suc 1 𝑜 On
46 45 onordi Ord suc 1 𝑜
47 1oex 1 𝑜 V
48 47 sucid 1 𝑜 suc 1 𝑜
49 nordeq Ord suc 1 𝑜 1 𝑜 suc 1 𝑜 suc 1 𝑜 1 𝑜
50 46 48 49 mp2an suc 1 𝑜 1 𝑜
51 43 50 eqnetri 2 𝑜 1 𝑜
52 51 nesymi ¬ 1 𝑜 = 2 𝑜
53 eqtr2 A X x = 1 𝑜 A X x = 2 𝑜 1 𝑜 = 2 𝑜
54 52 53 mto ¬ A X x = 1 𝑜 A X x = 2 𝑜
55 2on0 2 𝑜
56 55 nesymi ¬ = 2 𝑜
57 eqtr2 A X x = A X x = 2 𝑜 = 2 𝑜
58 56 57 mto ¬ A X x = A X x = 2 𝑜
59 42 54 58 3pm3.2i ¬ A X x = 1 𝑜 A X x = ¬ A X x = 1 𝑜 A X x = 2 𝑜 ¬ A X x = A X x = 2 𝑜
60 fvex A X x V
61 60 60 brtp A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 A X x A X x = 1 𝑜 A X x = A X x = 1 𝑜 A X x = 2 𝑜 A X x = A X x = 2 𝑜
62 3oran A X x = 1 𝑜 A X x = A X x = 1 𝑜 A X x = 2 𝑜 A X x = A X x = 2 𝑜 ¬ ¬ A X x = 1 𝑜 A X x = ¬ A X x = 1 𝑜 A X x = 2 𝑜 ¬ A X x = A X x = 2 𝑜
63 61 62 bitri A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 A X x ¬ ¬ A X x = 1 𝑜 A X x = ¬ A X x = 1 𝑜 A X x = 2 𝑜 ¬ A X x = A X x = 2 𝑜
64 63 con2bii ¬ A X x = 1 𝑜 A X x = ¬ A X x = 1 𝑜 A X x = 2 𝑜 ¬ A X x = A X x = 2 𝑜 ¬ A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 A X x
65 59 64 mpbi ¬ A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 A X x
66 simpl2l A No B No X On A X = B X A < s B B X = A X = 2 𝑜 A X = B X
67 66 adantr A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y A X = B X
68 67 fveq1d A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y A X x = B X x
69 68 breq2d A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 A X x A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X x
70 65 69 mtbii A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y ¬ A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X x
71 fvres x X A X x = A x
72 fvres x X B X x = B x
73 71 72 breq12d x X A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X x A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
74 73 notbid x X ¬ A X x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X x ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
75 70 74 syl5ibcom A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y x X ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
76 51 neii ¬ 2 𝑜 = 1 𝑜
77 76 intnanr ¬ 2 𝑜 = 1 𝑜 =
78 56 intnan ¬ 2 𝑜 = 1 𝑜 = 2 𝑜
79 56 intnan ¬ 2 𝑜 = = 2 𝑜
80 77 78 79 3pm3.2i ¬ 2 𝑜 = 1 𝑜 = ¬ 2 𝑜 = 1 𝑜 = 2 𝑜 ¬ 2 𝑜 = = 2 𝑜
81 2oex 2 𝑜 V
82 0ex V
83 81 82 brtp 2 𝑜 1 𝑜 1 𝑜 2 𝑜 2 𝑜 2 𝑜 = 1 𝑜 = 2 𝑜 = 1 𝑜 = 2 𝑜 2 𝑜 = = 2 𝑜
84 3oran 2 𝑜 = 1 𝑜 = 2 𝑜 = 1 𝑜 = 2 𝑜 2 𝑜 = = 2 𝑜 ¬ ¬ 2 𝑜 = 1 𝑜 = ¬ 2 𝑜 = 1 𝑜 = 2 𝑜 ¬ 2 𝑜 = = 2 𝑜
85 83 84 bitri 2 𝑜 1 𝑜 1 𝑜 2 𝑜 2 𝑜 ¬ ¬ 2 𝑜 = 1 𝑜 = ¬ 2 𝑜 = 1 𝑜 = 2 𝑜 ¬ 2 𝑜 = = 2 𝑜
86 85 con2bii ¬ 2 𝑜 = 1 𝑜 = ¬ 2 𝑜 = 1 𝑜 = 2 𝑜 ¬ 2 𝑜 = = 2 𝑜 ¬ 2 𝑜 1 𝑜 1 𝑜 2 𝑜 2 𝑜
87 80 86 mpbi ¬ 2 𝑜 1 𝑜 1 𝑜 2 𝑜 2 𝑜
88 simplr A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y A X = 2 𝑜
89 simpll3 A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y B X =
90 88 89 breq12d A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y A X 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X 2 𝑜 1 𝑜 1 𝑜 2 𝑜 2 𝑜
91 87 90 mtbiri A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y ¬ A X 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X
92 fveq2 x = X A x = A X
93 fveq2 x = X B x = B X
94 92 93 breq12d x = X A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x A X 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X
95 94 notbid x = X ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x ¬ A X 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B X
96 91 95 syl5ibrcom A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y x = X ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
97 fveq2 y = X A y = A X
98 fveq2 y = X B y = B X
99 97 98 eqeq12d y = X A y = B y A X = B X
100 99 rspccv y x A y = B y X x A X = B X
101 100 ad2antll A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y X x A X = B X
102 eqcom A X = B X B X = A X
103 101 102 syl6ib A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y X x B X = A X
104 89 88 eqeq12d A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y B X = A X = 2 𝑜
105 103 104 sylibd A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y X x = 2 𝑜
106 56 105 mtoi A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y ¬ X x
107 simprl A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y x On
108 simpl13 A No B No X On A X = B X A < s B B X = A X = 2 𝑜 X On
109 108 adantr A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y X On
110 ontri1 x On X On x X ¬ X x
111 onsseleq x On X On x X x X x = X
112 110 111 bitr3d x On X On ¬ X x x X x = X
113 107 109 112 syl2anc A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y ¬ X x x X x = X
114 106 113 mpbid A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y x X x = X
115 75 96 114 mpjaod A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
116 115 expr A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
117 116 ralrimiva A No B No X On A X = B X A < s B B X = A X = 2 𝑜 x On y x A y = B y ¬ A x 1 𝑜 1 𝑜 2 𝑜 2 𝑜 B x
118 38 117 mtand A No B No X On A X = B X A < s B B X = ¬ A X = 2 𝑜
119 nofv A No A X = A X = 1 𝑜 A X = 2 𝑜
120 2 119 syl A No B No X On A X = B X A < s B B X = A X = A X = 1 𝑜 A X = 2 𝑜
121 3orcoma A X = A X = 1 𝑜 A X = 2 𝑜 A X = 1 𝑜 A X = A X = 2 𝑜
122 120 121 sylib A No B No X On A X = B X A < s B B X = A X = 1 𝑜 A X = A X = 2 𝑜
123 30 118 122 ecase23d A No B No X On A X = B X A < s B B X = A X = 1 𝑜