| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elvv 5760 | . . 3
⊢ (𝐴 ∈ (V × V) ↔
∃𝑤∃𝑣 𝐴 = 〈𝑤, 𝑣〉) | 
| 2 |  | fveq2 6906 | . . . . . 6
⊢ (𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘〈𝑤, 𝑣〉)) | 
| 3 |  | df-ov 7434 | . . . . . . 7
⊢ (𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}𝑣) = ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘〈𝑤, 𝑣〉) | 
| 4 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑣) → 𝑥 = 𝑤) | 
| 5 |  | mpov 7545 | . . . . . . . . . 10
⊢ (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝑥) = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} | 
| 6 | 5 | eqcomi 2746 | . . . . . . . . 9
⊢
{〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} = (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝑥) | 
| 7 |  | vex 3484 | . . . . . . . . 9
⊢ 𝑤 ∈ V | 
| 8 | 4, 6, 7 | ovmpoa 7588 | . . . . . . . 8
⊢ ((𝑤 ∈ V ∧ 𝑣 ∈ V) → (𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}𝑣) = 𝑤) | 
| 9 | 8 | el2v 3487 | . . . . . . 7
⊢ (𝑤{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}𝑣) = 𝑤 | 
| 10 | 3, 9 | eqtr3i 2767 | . . . . . 6
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘〈𝑤, 𝑣〉) = 𝑤 | 
| 11 | 2, 10 | eqtrdi 2793 | . . . . 5
⊢ (𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = 𝑤) | 
| 12 |  | vex 3484 | . . . . . 6
⊢ 𝑣 ∈ V | 
| 13 | 7, 12 | op1std 8024 | . . . . 5
⊢ (𝐴 = 〈𝑤, 𝑣〉 → (1st ‘𝐴) = 𝑤) | 
| 14 | 11, 13 | eqtr4d 2780 | . . . 4
⊢ (𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = (1st ‘𝐴)) | 
| 15 | 14 | exlimivv 1932 | . . 3
⊢
(∃𝑤∃𝑣 𝐴 = 〈𝑤, 𝑣〉 → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = (1st ‘𝐴)) | 
| 16 | 1, 15 | sylbi 217 | . 2
⊢ (𝐴 ∈ (V × V) →
({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = (1st ‘𝐴)) | 
| 17 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑥 ∈ V | 
| 18 |  | vex 3484 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 19 | 17, 18 | pm3.2i 470 | . . . . . . . . 9
⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V) | 
| 20 |  | ax6ev 1969 | . . . . . . . . 9
⊢
∃𝑧 𝑧 = 𝑥 | 
| 21 | 19, 20 | 2th 264 | . . . . . . . 8
⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) ↔ ∃𝑧 𝑧 = 𝑥) | 
| 22 | 21 | opabbii 5210 | . . . . . . 7
⊢
{〈𝑥, 𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 𝑧 = 𝑥} | 
| 23 |  | df-xp 5691 | . . . . . . 7
⊢ (V
× V) = {〈𝑥,
𝑦〉 ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} | 
| 24 |  | dmoprab 7536 | . . . . . . 7
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 𝑧 = 𝑥} | 
| 25 | 22, 23, 24 | 3eqtr4ri 2776 | . . . . . 6
⊢ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} = (V × V) | 
| 26 | 25 | eleq2i 2833 | . . . . 5
⊢ (𝐴 ∈ dom {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} ↔ 𝐴 ∈ (V × V)) | 
| 27 |  | ndmfv 6941 | . . . . 5
⊢ (¬
𝐴 ∈ dom
{〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥} → ({〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = ∅) | 
| 28 | 26, 27 | sylnbir 331 | . . . 4
⊢ (¬
𝐴 ∈ (V × V)
→ ({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = ∅) | 
| 29 |  | dmsnn0 6227 | . . . . . . . 8
⊢ (𝐴 ∈ (V × V) ↔ dom
{𝐴} ≠
∅) | 
| 30 | 29 | biimpri 228 | . . . . . . 7
⊢ (dom
{𝐴} ≠ ∅ →
𝐴 ∈ (V ×
V)) | 
| 31 | 30 | necon1bi 2969 | . . . . . 6
⊢ (¬
𝐴 ∈ (V × V)
→ dom {𝐴} =
∅) | 
| 32 | 31 | unieqd 4920 | . . . . 5
⊢ (¬
𝐴 ∈ (V × V)
→ ∪ dom {𝐴} = ∪
∅) | 
| 33 |  | uni0 4935 | . . . . 5
⊢ ∪ ∅ = ∅ | 
| 34 | 32, 33 | eqtrdi 2793 | . . . 4
⊢ (¬
𝐴 ∈ (V × V)
→ ∪ dom {𝐴} = ∅) | 
| 35 | 28, 34 | eqtr4d 2780 | . . 3
⊢ (¬
𝐴 ∈ (V × V)
→ ({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = ∪ dom {𝐴}) | 
| 36 |  | 1stval 8016 | . . 3
⊢
(1st ‘𝐴) = ∪ dom {𝐴} | 
| 37 | 35, 36 | eqtr4di 2795 | . 2
⊢ (¬
𝐴 ∈ (V × V)
→ ({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = (1st ‘𝐴)) | 
| 38 | 16, 37 | pm2.61i 182 | 1
⊢
({〈〈𝑥,
𝑦〉, 𝑧〉 ∣ 𝑧 = 𝑥}‘𝐴) = (1st ‘𝐴) |