Step | Hyp | Ref
| Expression |
1 | | elvv 5177 |
. . 3
⊢ (𝐴 ∈ (V × V) ↔
∃𝑤∃𝑣 𝐴 = 〈𝑤, 𝑣〉) |
2 | | fveq2 6191 |
. . . . . 6
⊢ (𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘〈𝑤, 𝑣〉)) |
3 | | df-ov 6653 |
. . . . . . 7
⊢ (𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}𝑣) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘〈𝑤, 𝑣〉) |
4 | | vex 3203 |
. . . . . . . 8
⊢ 𝑤 ∈ V |
5 | | vex 3203 |
. . . . . . . 8
⊢ 𝑣 ∈ V |
6 | | simpr 477 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → 𝑦 = 𝑣) |
7 | | mpt2v 6750 |
. . . . . . . . . 10
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝑦) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} |
8 | 7 | eqcomi 2631 |
. . . . . . . . 9
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} = (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝑦) |
9 | 6, 8, 5 | ovmpt2a 6791 |
. . . . . . . 8
⊢ ((𝑤 ∈ V ∧ 𝑣 ∈ V) → (𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}𝑣) = 𝑣) |
10 | 4, 5, 9 | mp2an 708 |
. . . . . . 7
⊢ (𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}𝑣) = 𝑣 |
11 | 3, 10 | eqtr3i 2646 |
. . . . . 6
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘〈𝑤, 𝑣〉) = 𝑣 |
12 | 2, 11 | syl6eq 2672 |
. . . . 5
⊢ (𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = 𝑣) |
13 | 4, 5 | op2ndd 7179 |
. . . . 5
⊢ (𝐴 = 〈𝑤, 𝑣〉 → (2nd ‘𝐴) = 𝑣) |
14 | 12, 13 | eqtr4d 2659 |
. . . 4
⊢ (𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = (2nd ‘𝐴)) |
15 | 14 | exlimivv 1860 |
. . 3
⊢
(∃𝑤∃𝑣 𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = (2nd ‘𝐴)) |
16 | 1, 15 | sylbi 207 |
. 2
⊢ (𝐴 ∈ (V × V) →
({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = (2nd ‘𝐴)) |
17 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
18 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
19 | 17, 18 | pm3.2i 471 |
. . . . . . . . 9
⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V) |
20 | | ax6ev 1890 |
. . . . . . . . 9
⊢
∃𝑧 𝑧 = 𝑦 |
21 | 19, 20 | 2th 254 |
. . . . . . . 8
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) ↔ ∃𝑧 𝑧 = 𝑦) |
22 | 21 | opabbii 4717 |
. . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 𝑧 = 𝑦} |
23 | | df-xp 5120 |
. . . . . . 7
⊢ (V
× V) = {〈𝑥,
𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} |
24 | | dmoprab 6741 |
. . . . . . 7
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 𝑧 = 𝑦} |
25 | 22, 23, 24 | 3eqtr4ri 2655 |
. . . . . 6
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} = (V × V) |
26 | 25 | eleq2i 2693 |
. . . . 5
⊢ (𝐴 ∈ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} ↔ 𝐴 ∈ (V × V)) |
27 | | ndmfv 6218 |
. . . . 5
⊢ (¬
𝐴 ∈ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦} → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = ∅) |
28 | 26, 27 | sylnbir 321 |
. . . 4
⊢ (¬
𝐴 ∈ (V × V)
→ ({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = ∅) |
29 | | rnsnn0 5601 |
. . . . . . . 8
⊢ (𝐴 ∈ (V × V) ↔ ran
{𝐴} ≠
∅) |
30 | 29 | biimpri 218 |
. . . . . . 7
⊢ (ran
{𝐴} ≠ ∅ →
𝐴 ∈ (V ×
V)) |
31 | 30 | necon1bi 2822 |
. . . . . 6
⊢ (¬
𝐴 ∈ (V × V)
→ ran {𝐴} =
∅) |
32 | 31 | unieqd 4446 |
. . . . 5
⊢ (¬
𝐴 ∈ (V × V)
→ ∪ ran {𝐴} = ∪
∅) |
33 | | uni0 4465 |
. . . . 5
⊢ ∪ ∅ = ∅ |
34 | 32, 33 | syl6eq 2672 |
. . . 4
⊢ (¬
𝐴 ∈ (V × V)
→ ∪ ran {𝐴} = ∅) |
35 | 28, 34 | eqtr4d 2659 |
. . 3
⊢ (¬
𝐴 ∈ (V × V)
→ ({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = ∪ ran {𝐴}) |
36 | | 2ndval 7171 |
. . 3
⊢
(2nd ‘𝐴) = ∪ ran {𝐴} |
37 | 35, 36 | syl6eqr 2674 |
. 2
⊢ (¬
𝐴 ∈ (V × V)
→ ({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = (2nd ‘𝐴)) |
38 | 16, 37 | pm2.61i 176 |
1
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑦}‘𝐴) = (2nd ‘𝐴) |