Metamath Proof Explorer


Theorem wemappo

Description: Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values.

Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by AV, 21-Jul-2024)

Ref Expression
Hypothesis wemapso.t T = x y | z A x z S y z w A w R z x w = y w
Assertion wemappo R Or A S Po B T Po B A

Proof

Step Hyp Ref Expression
1 wemapso.t T = x y | z A x z S y z w A w R z x w = y w
2 simpllr R Or A S Po B a B A b A S Po B
3 elmapi a B A a : A B
4 3 adantl R Or A S Po B a B A a : A B
5 4 ffvelrnda R Or A S Po B a B A b A a b B
6 poirr S Po B a b B ¬ a b S a b
7 2 5 6 syl2anc R Or A S Po B a B A b A ¬ a b S a b
8 7 intnanrd R Or A S Po B a B A b A ¬ a b S a b c A c R b a c = a c
9 8 nrexdv R Or A S Po B a B A ¬ b A a b S a b c A c R b a c = a c
10 1 wemaplem1 a V a V a T a b A a b S a b c A c R b a c = a c
11 10 el2v a T a b A a b S a b c A c R b a c = a c
12 9 11 sylnibr R Or A S Po B a B A ¬ a T a
13 simplr1 R Or A S Po B a B A b B A c B A a T b b T c a B A
14 simplr2 R Or A S Po B a B A b B A c B A a T b b T c b B A
15 simplr3 R Or A S Po B a B A b B A c B A a T b b T c c B A
16 simplll R Or A S Po B a B A b B A c B A a T b b T c R Or A
17 simpllr R Or A S Po B a B A b B A c B A a T b b T c S Po B
18 simprl R Or A S Po B a B A b B A c B A a T b b T c a T b
19 simprr R Or A S Po B a B A b B A c B A a T b b T c b T c
20 1 13 14 15 16 17 18 19 wemaplem3 R Or A S Po B a B A b B A c B A a T b b T c a T c
21 20 ex R Or A S Po B a B A b B A c B A a T b b T c a T c
22 12 21 ispod R Or A S Po B T Po B A