Step | Hyp | Ref
| Expression |
1 | | elxp 5657 |
. 2
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
2 | | sneq 4597 |
. . . . . . . . . . . 12
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → {𝐴} = {⟨𝑥, 𝑦⟩}) |
3 | 2 | rneqd 5894 |
. . . . . . . . . . 11
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ran {𝐴} = ran {⟨𝑥, 𝑦⟩}) |
4 | 3 | unieqd 4880 |
. . . . . . . . . 10
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → ∪
ran {𝐴} = ∪ ran {⟨𝑥, 𝑦⟩}) |
5 | | vex 3450 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
6 | | vex 3450 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
7 | 5, 6 | op2nda 6181 |
. . . . . . . . . 10
⊢ ∪ ran {⟨𝑥, 𝑦⟩} = 𝑦 |
8 | 4, 7 | eqtr2di 2794 |
. . . . . . . . 9
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ → 𝑦 = ∪ ran {𝐴}) |
9 | 8 | pm4.71ri 562 |
. . . . . . . 8
⊢ (𝐴 = ⟨𝑥, 𝑦⟩ ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩)) |
10 | 9 | anbi1i 625 |
. . . . . . 7
⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
11 | | anass 470 |
. . . . . . 7
⊢ (((𝑦 = ∪
ran {𝐴} ∧ 𝐴 = ⟨𝑥, 𝑦⟩) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
12 | 10, 11 | bitri 275 |
. . . . . 6
⊢ ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
13 | 12 | exbii 1851 |
. . . . 5
⊢
(∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
14 | | snex 5389 |
. . . . . . . 8
⊢ {𝐴} ∈ V |
15 | 14 | rnex 7850 |
. . . . . . 7
⊢ ran
{𝐴} ∈
V |
16 | 15 | uniex 7679 |
. . . . . 6
⊢ ∪ ran {𝐴} ∈ V |
17 | | opeq2 4832 |
. . . . . . . 8
⊢ (𝑦 = ∪
ran {𝐴} → ⟨𝑥, 𝑦⟩ = ⟨𝑥, ∪ ran {𝐴}⟩) |
18 | 17 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = ∪
ran {𝐴} → (𝐴 = ⟨𝑥, 𝑦⟩ ↔ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩)) |
19 | | eleq1 2826 |
. . . . . . . 8
⊢ (𝑦 = ∪
ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran
{𝐴} ∈ 𝐶)) |
20 | 19 | anbi2d 630 |
. . . . . . 7
⊢ (𝑦 = ∪
ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
21 | 18, 20 | anbi12d 632 |
. . . . . 6
⊢ (𝑦 = ∪
ran {𝐴} → ((𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
22 | 16, 21 | ceqsexv 3495 |
. . . . 5
⊢
(∃𝑦(𝑦 = ∪
ran {𝐴} ∧ (𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
23 | 13, 22 | bitri 275 |
. . . 4
⊢
(∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
24 | | sneq 4597 |
. . . . . . . . 9
⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → {𝐴} = {⟨𝑥, ∪ ran {𝐴}⟩}) |
25 | 24 | dmeqd 5862 |
. . . . . . . 8
⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → dom {𝐴} = dom {⟨𝑥, ∪
ran {𝐴}⟩}) |
26 | 25 | unieqd 4880 |
. . . . . . 7
⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → ∪ dom {𝐴} = ∪ dom
{⟨𝑥, ∪ ran {𝐴}⟩}) |
27 | 5, 16 | op1sta 6178 |
. . . . . . 7
⊢ ∪ dom {⟨𝑥, ∪ ran {𝐴}⟩} = 𝑥 |
28 | 26, 27 | eqtr2di 2794 |
. . . . . 6
⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ → 𝑥 = ∪
dom {𝐴}) |
29 | 28 | pm4.71ri 562 |
. . . . 5
⊢ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ (𝑥 = ∪
dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩)) |
30 | 29 | anbi1i 625 |
. . . 4
⊢ ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∪ dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
31 | | anass 470 |
. . . 4
⊢ (((𝑥 = ∪
dom {𝐴} ∧ 𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
32 | 23, 30, 31 | 3bitri 297 |
. . 3
⊢
(∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
33 | 32 | exbii 1851 |
. 2
⊢
(∃𝑥∃𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∪ dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
34 | 14 | dmex 7849 |
. . . 4
⊢ dom
{𝐴} ∈
V |
35 | 34 | uniex 7679 |
. . 3
⊢ ∪ dom {𝐴} ∈ V |
36 | | opeq1 4831 |
. . . . 5
⊢ (𝑥 = ∪
dom {𝐴} → ⟨𝑥, ∪
ran {𝐴}⟩ = ⟨∪ dom {𝐴}, ∪ ran {𝐴}⟩) |
37 | 36 | eqeq2d 2748 |
. . . 4
⊢ (𝑥 = ∪
dom {𝐴} → (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ↔ 𝐴 = ⟨∪ dom
{𝐴}, ∪ ran {𝐴}⟩)) |
38 | | eleq1 2826 |
. . . . 5
⊢ (𝑥 = ∪
dom {𝐴} → (𝑥 ∈ 𝐵 ↔ ∪ dom
{𝐴} ∈ 𝐵)) |
39 | 38 | anbi1d 631 |
. . . 4
⊢ (𝑥 = ∪
dom {𝐴} → ((𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶) ↔ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
40 | 37, 39 | anbi12d 632 |
. . 3
⊢ (𝑥 = ∪
dom {𝐴} → ((𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ (𝐴 = ⟨∪ dom
{𝐴}, ∪ ran {𝐴}⟩ ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶)))) |
41 | 35, 40 | ceqsexv 3495 |
. 2
⊢
(∃𝑥(𝑥 = ∪
dom {𝐴} ∧ (𝐴 = ⟨𝑥, ∪ ran {𝐴}⟩ ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) ↔ (𝐴 = ⟨∪ dom
{𝐴}, ∪ ran {𝐴}⟩ ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |
42 | 1, 33, 41 | 3bitri 297 |
1
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = ⟨∪ dom
{𝐴}, ∪ ran {𝐴}⟩ ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |