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=xy|zAxzSyzwAwRzxw=yw
Assertion wemappo ROrASPoBTPoBA

Proof

Step Hyp Ref Expression
1 wemapso.t T=xy|zAxzSyzwAwRzxw=yw
2 simpllr ROrASPoBaBAbASPoB
3 elmapi aBAa:AB
4 3 adantl ROrASPoBaBAa:AB
5 4 ffvelrnda ROrASPoBaBAbAabB
6 poirr SPoBabB¬abSab
7 2 5 6 syl2anc ROrASPoBaBAbA¬abSab
8 7 intnanrd ROrASPoBaBAbA¬abSabcAcRbac=ac
9 8 nrexdv ROrASPoBaBA¬bAabSabcAcRbac=ac
10 1 wemaplem1 aVaVaTabAabSabcAcRbac=ac
11 10 el2v aTabAabSabcAcRbac=ac
12 9 11 sylnibr ROrASPoBaBA¬aTa
13 simplr1 ROrASPoBaBAbBAcBAaTbbTcaBA
14 simplr2 ROrASPoBaBAbBAcBAaTbbTcbBA
15 simplr3 ROrASPoBaBAbBAcBAaTbbTccBA
16 simplll ROrASPoBaBAbBAcBAaTbbTcROrA
17 simpllr ROrASPoBaBAbBAcBAaTbbTcSPoB
18 simprl ROrASPoBaBAbBAcBAaTbbTcaTb
19 simprr ROrASPoBaBAbBAcBAaTbbTcbTc
20 1 13 14 15 16 17 18 19 wemaplem3 ROrASPoBaBAbBAcBAaTbbTcaTc
21 20 ex ROrASPoBaBAbBAcBAaTbbTcaTc
22 12 21 ispod ROrASPoBTPoBA