Metamath Proof Explorer

Theorem wemaplem1

Description: Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypothesis wemapso.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
Assertion wemaplem1 ( ( 𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊 ) → ( 𝑃 𝑇 𝑄 ↔ ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ∧ ∀ 𝑏 ∈ 𝐴 ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 wemapso.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
2 fveq1 ⊢ ( 𝑥 = 𝑃 → ( 𝑥 ‘ 𝑧 ) = ( 𝑃 ‘ 𝑧 ) )
3 fveq1 ⊢ ( 𝑦 = 𝑄 → ( 𝑦 ‘ 𝑧 ) = ( 𝑄 ‘ 𝑧 ) )
4 2 3 breqan12d ⊢ ( ( 𝑥 = 𝑃 ∧ 𝑦 = 𝑄 ) → ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ↔ ( 𝑃 ‘ 𝑧 ) 𝑆 ( 𝑄 ‘ 𝑧 ) ) )
5 fveq1 ⊢ ( 𝑥 = 𝑃 → ( 𝑥 ‘ 𝑤 ) = ( 𝑃 ‘ 𝑤 ) )
6 fveq1 ⊢ ( 𝑦 = 𝑄 → ( 𝑦 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) )
7 5 6 eqeqan12d ⊢ ( ( 𝑥 = 𝑃 ∧ 𝑦 = 𝑄 ) → ( ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ↔ ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) )
8 7 imbi2d ⊢ ( ( 𝑥 = 𝑃 ∧ 𝑦 = 𝑄 ) → ( ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) )
9 8 ralbidv ⊢ ( ( 𝑥 = 𝑃 ∧ 𝑦 = 𝑄 ) → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) )
10 4 9 anbi12d ⊢ ( ( 𝑥 = 𝑃 ∧ 𝑦 = 𝑄 ) → ( ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ( ( 𝑃 ‘ 𝑧 ) 𝑆 ( 𝑄 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) ) )
11 10 rexbidv ⊢ ( ( 𝑥 = 𝑃 ∧ 𝑦 = 𝑄 ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑧 ∈ 𝐴 ( ( 𝑃 ‘ 𝑧 ) 𝑆 ( 𝑄 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) ) )
12 fveq2 ⊢ ( 𝑧 = 𝑎 → ( 𝑃 ‘ 𝑧 ) = ( 𝑃 ‘ 𝑎 ) )
13 fveq2 ⊢ ( 𝑧 = 𝑎 → ( 𝑄 ‘ 𝑧 ) = ( 𝑄 ‘ 𝑎 ) )
14 12 13 breq12d ⊢ ( 𝑧 = 𝑎 → ( ( 𝑃 ‘ 𝑧 ) 𝑆 ( 𝑄 ‘ 𝑧 ) ↔ ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ) )
15 breq2 ⊢ ( 𝑧 = 𝑎 → ( 𝑤 𝑅 𝑧 ↔ 𝑤 𝑅 𝑎 ) )
16 15 imbi1d ⊢ ( 𝑧 = 𝑎 → ( ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ↔ ( 𝑤 𝑅 𝑎 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) )
17 16 ralbidv ⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ↔ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑎 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) )
18 breq1 ⊢ ( 𝑤 = 𝑏 → ( 𝑤 𝑅 𝑎 ↔ 𝑏 𝑅 𝑎 ) )
19 fveq2 ⊢ ( 𝑤 = 𝑏 → ( 𝑃 ‘ 𝑤 ) = ( 𝑃 ‘ 𝑏 ) )
20 fveq2 ⊢ ( 𝑤 = 𝑏 → ( 𝑄 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑏 ) )
21 19 20 eqeq12d ⊢ ( 𝑤 = 𝑏 → ( ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ↔ ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) )
22 18 21 imbi12d ⊢ ( 𝑤 = 𝑏 → ( ( 𝑤 𝑅 𝑎 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ↔ ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) ) )
23 22 cbvralvw ⊢ ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑎 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ↔ ∀ 𝑏 ∈ 𝐴 ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) )
24 17 23 bitrdi ⊢ ( 𝑧 = 𝑎 → ( ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ↔ ∀ 𝑏 ∈ 𝐴 ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) ) )
25 14 24 anbi12d ⊢ ( 𝑧 = 𝑎 → ( ( ( 𝑃 ‘ 𝑧 ) 𝑆 ( 𝑄 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) ↔ ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ∧ ∀ 𝑏 ∈ 𝐴 ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) ) ) )
26 25 cbvrexvw ⊢ ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑃 ‘ 𝑧 ) 𝑆 ( 𝑄 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑃 ‘ 𝑤 ) = ( 𝑄 ‘ 𝑤 ) ) ) ↔ ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ∧ ∀ 𝑏 ∈ 𝐴 ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) ) )
27 11 26 bitrdi ⊢ ( ( 𝑥 = 𝑃 ∧ 𝑦 = 𝑄 ) → ( ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) ↔ ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ∧ ∀ 𝑏 ∈ 𝐴 ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) ) ) )
28 27 1 brabga ⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊 ) → ( 𝑃 𝑇 𝑄 ↔ ∃ 𝑎 ∈ 𝐴 ( ( 𝑃 ‘ 𝑎 ) 𝑆 ( 𝑄 ‘ 𝑎 ) ∧ ∀ 𝑏 ∈ 𝐴 ( 𝑏 𝑅 𝑎 → ( 𝑃 ‘ 𝑏 ) = ( 𝑄 ‘ 𝑏 ) ) ) ) )