Proof of Theorem wemaplem1
Step | Hyp | Ref
| Expression |
1 | | fveq1 6673 |
. . . . . 6
⊢ (𝑥 = 𝑃 → (𝑥‘𝑧) = (𝑃‘𝑧)) |
2 | | fveq1 6673 |
. . . . . 6
⊢ (𝑦 = 𝑄 → (𝑦‘𝑧) = (𝑄‘𝑧)) |
3 | 1, 2 | breqan12d 5046 |
. . . . 5
⊢ ((𝑥 = 𝑃 ∧ 𝑦 = 𝑄) → ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ↔ (𝑃‘𝑧)𝑆(𝑄‘𝑧))) |
4 | | fveq1 6673 |
. . . . . . . 8
⊢ (𝑥 = 𝑃 → (𝑥‘𝑤) = (𝑃‘𝑤)) |
5 | | fveq1 6673 |
. . . . . . . 8
⊢ (𝑦 = 𝑄 → (𝑦‘𝑤) = (𝑄‘𝑤)) |
6 | 4, 5 | eqeqan12d 2755 |
. . . . . . 7
⊢ ((𝑥 = 𝑃 ∧ 𝑦 = 𝑄) → ((𝑥‘𝑤) = (𝑦‘𝑤) ↔ (𝑃‘𝑤) = (𝑄‘𝑤))) |
7 | 6 | imbi2d 344 |
. . . . . 6
⊢ ((𝑥 = 𝑃 ∧ 𝑦 = 𝑄) → ((𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤)))) |
8 | 7 | ralbidv 3109 |
. . . . 5
⊢ ((𝑥 = 𝑃 ∧ 𝑦 = 𝑄) → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤)))) |
9 | 3, 8 | anbi12d 634 |
. . . 4
⊢ ((𝑥 = 𝑃 ∧ 𝑦 = 𝑄) → (((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ((𝑃‘𝑧)𝑆(𝑄‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤))))) |
10 | 9 | rexbidv 3207 |
. . 3
⊢ ((𝑥 = 𝑃 ∧ 𝑦 = 𝑄) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑧 ∈ 𝐴 ((𝑃‘𝑧)𝑆(𝑄‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤))))) |
11 | | fveq2 6674 |
. . . . . 6
⊢ (𝑧 = 𝑎 → (𝑃‘𝑧) = (𝑃‘𝑎)) |
12 | | fveq2 6674 |
. . . . . 6
⊢ (𝑧 = 𝑎 → (𝑄‘𝑧) = (𝑄‘𝑎)) |
13 | 11, 12 | breq12d 5043 |
. . . . 5
⊢ (𝑧 = 𝑎 → ((𝑃‘𝑧)𝑆(𝑄‘𝑧) ↔ (𝑃‘𝑎)𝑆(𝑄‘𝑎))) |
14 | | breq2 5034 |
. . . . . . . 8
⊢ (𝑧 = 𝑎 → (𝑤𝑅𝑧 ↔ 𝑤𝑅𝑎)) |
15 | 14 | imbi1d 345 |
. . . . . . 7
⊢ (𝑧 = 𝑎 → ((𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤)) ↔ (𝑤𝑅𝑎 → (𝑃‘𝑤) = (𝑄‘𝑤)))) |
16 | 15 | ralbidv 3109 |
. . . . . 6
⊢ (𝑧 = 𝑎 → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤)) ↔ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑎 → (𝑃‘𝑤) = (𝑄‘𝑤)))) |
17 | | breq1 5033 |
. . . . . . . 8
⊢ (𝑤 = 𝑏 → (𝑤𝑅𝑎 ↔ 𝑏𝑅𝑎)) |
18 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑤 = 𝑏 → (𝑃‘𝑤) = (𝑃‘𝑏)) |
19 | | fveq2 6674 |
. . . . . . . . 9
⊢ (𝑤 = 𝑏 → (𝑄‘𝑤) = (𝑄‘𝑏)) |
20 | 18, 19 | eqeq12d 2754 |
. . . . . . . 8
⊢ (𝑤 = 𝑏 → ((𝑃‘𝑤) = (𝑄‘𝑤) ↔ (𝑃‘𝑏) = (𝑄‘𝑏))) |
21 | 17, 20 | imbi12d 348 |
. . . . . . 7
⊢ (𝑤 = 𝑏 → ((𝑤𝑅𝑎 → (𝑃‘𝑤) = (𝑄‘𝑤)) ↔ (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏)))) |
22 | 21 | cbvralvw 3349 |
. . . . . 6
⊢
(∀𝑤 ∈
𝐴 (𝑤𝑅𝑎 → (𝑃‘𝑤) = (𝑄‘𝑤)) ↔ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏))) |
23 | 16, 22 | bitrdi 290 |
. . . . 5
⊢ (𝑧 = 𝑎 → (∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤)) ↔ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏)))) |
24 | 13, 23 | anbi12d 634 |
. . . 4
⊢ (𝑧 = 𝑎 → (((𝑃‘𝑧)𝑆(𝑄‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤))) ↔ ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏))))) |
25 | 24 | cbvrexvw 3350 |
. . 3
⊢
(∃𝑧 ∈
𝐴 ((𝑃‘𝑧)𝑆(𝑄‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑃‘𝑤) = (𝑄‘𝑤))) ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏)))) |
26 | 10, 25 | bitrdi 290 |
. 2
⊢ ((𝑥 = 𝑃 ∧ 𝑦 = 𝑄) → (∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤))) ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏))))) |
27 | | wemapso.t |
. 2
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 ((𝑥‘𝑧)𝑆(𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐴 (𝑤𝑅𝑧 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
28 | 26, 27 | brabga 5389 |
1
⊢ ((𝑃 ∈ 𝑉 ∧ 𝑄 ∈ 𝑊) → (𝑃𝑇𝑄 ↔ ∃𝑎 ∈ 𝐴 ((𝑃‘𝑎)𝑆(𝑄‘𝑎) ∧ ∀𝑏 ∈ 𝐴 (𝑏𝑅𝑎 → (𝑃‘𝑏) = (𝑄‘𝑏))))) |