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 | ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } | |
| Assertion | wemappo | ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) → 𝑇 Po ( 𝐵 ↑m 𝐴 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wemapso.t | ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) } | |
| 2 | simpllr | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑏 ∈ 𝐴 ) → 𝑆 Po 𝐵 ) | |
| 3 | elmapi | ⊢ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) → 𝑎 : 𝐴 ⟶ 𝐵 ) | |
| 4 | 3 | adantl | ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) → 𝑎 : 𝐴 ⟶ 𝐵 ) |
| 5 | 4 | ffvelrnda | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑏 ∈ 𝐴 ) → ( 𝑎 ‘ 𝑏 ) ∈ 𝐵 ) |
| 6 | poirr | ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑎 ‘ 𝑏 ) ∈ 𝐵 ) → ¬ ( 𝑎 ‘ 𝑏 ) 𝑆 ( 𝑎 ‘ 𝑏 ) ) | |
| 7 | 2 5 6 | syl2anc | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑏 ∈ 𝐴 ) → ¬ ( 𝑎 ‘ 𝑏 ) 𝑆 ( 𝑎 ‘ 𝑏 ) ) |
| 8 | 7 | intnanrd | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) ∧ 𝑏 ∈ 𝐴 ) → ¬ ( ( 𝑎 ‘ 𝑏 ) 𝑆 ( 𝑎 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑎 ‘ 𝑐 ) = ( 𝑎 ‘ 𝑐 ) ) ) ) |
| 9 | 8 | nrexdv | ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) → ¬ ∃ 𝑏 ∈ 𝐴 ( ( 𝑎 ‘ 𝑏 ) 𝑆 ( 𝑎 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑎 ‘ 𝑐 ) = ( 𝑎 ‘ 𝑐 ) ) ) ) |
| 10 | 1 | wemaplem1 | ⊢ ( ( 𝑎 ∈ V ∧ 𝑎 ∈ V ) → ( 𝑎 𝑇 𝑎 ↔ ∃ 𝑏 ∈ 𝐴 ( ( 𝑎 ‘ 𝑏 ) 𝑆 ( 𝑎 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑎 ‘ 𝑐 ) = ( 𝑎 ‘ 𝑐 ) ) ) ) ) |
| 11 | 10 | el2v | ⊢ ( 𝑎 𝑇 𝑎 ↔ ∃ 𝑏 ∈ 𝐴 ( ( 𝑎 ‘ 𝑏 ) 𝑆 ( 𝑎 ‘ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝐴 ( 𝑐 𝑅 𝑏 → ( 𝑎 ‘ 𝑐 ) = ( 𝑎 ‘ 𝑐 ) ) ) ) |
| 12 | 9 11 | sylnibr | ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) → ¬ 𝑎 𝑇 𝑎 ) |
| 13 | simplr1 | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ) | |
| 14 | simplr2 | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ) | |
| 15 | simplr3 | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) | |
| 16 | simplll | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑅 Or 𝐴 ) | |
| 17 | simpllr | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑆 Po 𝐵 ) | |
| 18 | simprl | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑎 𝑇 𝑏 ) | |
| 19 | simprr | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑏 𝑇 𝑐 ) | |
| 20 | 1 13 14 15 16 17 18 19 | wemaplem3 | ⊢ ( ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) ∧ ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ) → 𝑎 𝑇 𝑐 ) |
| 21 | 20 | ex | ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑏 ∈ ( 𝐵 ↑m 𝐴 ) ∧ 𝑐 ∈ ( 𝐵 ↑m 𝐴 ) ) ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) |
| 22 | 12 21 | ispod | ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑆 Po 𝐵 ) → 𝑇 Po ( 𝐵 ↑m 𝐴 ) ) |