Proof of Theorem fvopab3ig
Step | Hyp | Ref
| Expression |
1 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐶 ↔ 𝐴 ∈ 𝐶)) |
2 | | fvopab3ig.1 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
3 | 1, 2 | anbi12d 631 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐶 ∧ 𝜑) ↔ (𝐴 ∈ 𝐶 ∧ 𝜓))) |
4 | | fvopab3ig.2 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (𝜓 ↔ 𝜒)) |
5 | 4 | anbi2d 629 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((𝐴 ∈ 𝐶 ∧ 𝜓) ↔ (𝐴 ∈ 𝐶 ∧ 𝜒))) |
6 | 3, 5 | opelopabg 5448 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} ↔ (𝐴 ∈ 𝐶 ∧ 𝜒))) |
7 | 6 | biimpar 478 |
. . . . 5
⊢ (((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) ∧ (𝐴 ∈ 𝐶 ∧ 𝜒)) → 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}) |
8 | 7 | exp43 437 |
. . . 4
⊢ (𝐴 ∈ 𝐶 → (𝐵 ∈ 𝐷 → (𝐴 ∈ 𝐶 → (𝜒 → 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)})))) |
9 | 8 | pm2.43a 54 |
. . 3
⊢ (𝐴 ∈ 𝐶 → (𝐵 ∈ 𝐷 → (𝜒 → 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}))) |
10 | 9 | imp 407 |
. 2
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝜒 → 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)})) |
11 | | fvopab3ig.4 |
. . . 4
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} |
12 | 11 | fveq1i 6767 |
. . 3
⊢ (𝐹‘𝐴) = ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}‘𝐴) |
13 | | funopab 6461 |
. . . . 5
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐶 ∧ 𝜑)) |
14 | | fvopab3ig.3 |
. . . . . 6
⊢ (𝑥 ∈ 𝐶 → ∃*𝑦𝜑) |
15 | | moanimv 2621 |
. . . . . 6
⊢
(∃*𝑦(𝑥 ∈ 𝐶 ∧ 𝜑) ↔ (𝑥 ∈ 𝐶 → ∃*𝑦𝜑)) |
16 | 14, 15 | mpbir 230 |
. . . . 5
⊢
∃*𝑦(𝑥 ∈ 𝐶 ∧ 𝜑) |
17 | 13, 16 | mpgbir 1802 |
. . . 4
⊢ Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} |
18 | | funopfv 6813 |
. . . 4
⊢ (Fun
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}‘𝐴) = 𝐵)) |
19 | 17, 18 | ax-mp 5 |
. . 3
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} → ({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)}‘𝐴) = 𝐵) |
20 | 12, 19 | eqtrid 2790 |
. 2
⊢
(〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐶 ∧ 𝜑)} → (𝐹‘𝐴) = 𝐵) |
21 | 10, 20 | syl6 35 |
1
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝜒 → (𝐹‘𝐴) = 𝐵)) |