Step | Hyp | Ref
| Expression |
1 | | elxp 5542 |
. 2
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
2 | | sneq 4523 |
. . . . . . . . . . . 12
⊢ (𝐴 = 〈𝑥, 𝑦〉 → {𝐴} = {〈𝑥, 𝑦〉}) |
3 | 2 | rneqd 5775 |
. . . . . . . . . . 11
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ran {𝐴} = ran {〈𝑥, 𝑦〉}) |
4 | 3 | unieqd 4807 |
. . . . . . . . . 10
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ∪
ran {𝐴} = ∪ ran {〈𝑥, 𝑦〉}) |
5 | | vex 3401 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
6 | | vex 3401 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
7 | 5, 6 | op2nda 6054 |
. . . . . . . . . 10
⊢ ∪ ran {〈𝑥, 𝑦〉} = 𝑦 |
8 | 4, 7 | eqtr2di 2790 |
. . . . . . . . 9
⊢ (𝐴 = 〈𝑥, 𝑦〉 → 𝑦 = ∪ ran {𝐴}) |
9 | 8 | pm4.71ri 564 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑥, 𝑦〉 ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = 〈𝑥, 𝑦〉)) |
10 | 9 | anbi1i 627 |
. . . . . . 7
⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = 〈𝑥, 𝑦〉) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
11 | | anass 472 |
. . . . . . 7
⊢ (((𝑦 = ∪
ran {𝐴} ∧ 𝐴 = 〈𝑥, 𝑦〉) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
12 | 10, 11 | bitri 278 |
. . . . . 6
⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
13 | 12 | exbii 1854 |
. . . . 5
⊢
(∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
14 | | snex 5295 |
. . . . . . . 8
⊢ {𝐴} ∈ V |
15 | 14 | rnex 7636 |
. . . . . . 7
⊢ ran
{𝐴} ∈
V |
16 | 15 | uniex 7479 |
. . . . . 6
⊢ ∪ ran {𝐴} ∈ V |
17 | | opeq2 4758 |
. . . . . . . 8
⊢ (𝑦 = ∪
ran {𝐴} → 〈𝑥, 𝑦〉 = 〈𝑥, ∪ ran {𝐴}〉) |
18 | 17 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑦 = ∪
ran {𝐴} → (𝐴 = 〈𝑥, 𝑦〉 ↔ 𝐴 = 〈𝑥, ∪ ran {𝐴}〉)) |
19 | | eleq1 2820 |
. . . . . . . 8
⊢ (𝑦 = ∪
ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran
{𝐴} ∈ 𝐶)) |
20 | 19 | anbi2d 632 |
. . . . . . 7
⊢ (𝑦 = ∪
ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
21 | 18, 20 | anbi12d 634 |
. . . . . 6
⊢ (𝑦 = ∪
ran {𝐴} → ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
22 | 16, 21 | ceqsexv 3444 |
. . . . 5
⊢
(∃𝑦(𝑦 = ∪
ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
23 | 13, 22 | bitri 278 |
. . . 4
⊢
(∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
24 | | inteq 4836 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 → ∩ 𝐴 =
∩ 〈𝑥, ∪ ran {𝐴}〉) |
25 | 24 | inteqd 4838 |
. . . . . . 7
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 → ∩ ∩ 𝐴 = ∩ ∩ 〈𝑥, ∪ ran {𝐴}〉) |
26 | 5, 16 | op1stb 5326 |
. . . . . . 7
⊢ ∩ ∩ 〈𝑥, ∪ ran {𝐴}〉 = 𝑥 |
27 | 25, 26 | eqtr2di 2790 |
. . . . . 6
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 → 𝑥 = ∩
∩ 𝐴) |
28 | 27 | pm4.71ri 564 |
. . . . 5
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ↔ (𝑥 = ∩
∩ 𝐴 ∧ 𝐴 = 〈𝑥, ∪ ran {𝐴}〉)) |
29 | 28 | anbi1i 627 |
. . . 4
⊢ ((𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∩ ∩ 𝐴
∧ 𝐴 = 〈𝑥, ∪
ran {𝐴}〉) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
30 | | anass 472 |
. . . 4
⊢ (((𝑥 = ∩
∩ 𝐴 ∧ 𝐴 = 〈𝑥, ∪ ran {𝐴}〉) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
31 | 23, 29, 30 | 3bitri 300 |
. . 3
⊢
(∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
32 | 31 | exbii 1854 |
. 2
⊢
(∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
33 | | eqvisset 3414 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝐴 → ∩ ∩ 𝐴
∈ V) |
34 | 33 | adantr 484 |
. . . 4
⊢ ((𝑥 = ∩
∩ 𝐴 ∧ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V) |
35 | 34 | exlimiv 1936 |
. . 3
⊢
(∃𝑥(𝑥 = ∩
∩ 𝐴 ∧ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V) |
36 | | elex 3415 |
. . . 4
⊢ (∩ ∩ 𝐴 ∈ 𝐵 → ∩ ∩ 𝐴
∈ V) |
37 | 36 | ad2antrl 728 |
. . 3
⊢ ((𝐴 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉 ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) → ∩ ∩ 𝐴 ∈ V) |
38 | | opeq1 4756 |
. . . . . 6
⊢ (𝑥 = ∩
∩ 𝐴 → 〈𝑥, ∪ ran {𝐴}〉 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉) |
39 | 38 | eqeq2d 2749 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝐴 → (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ↔ 𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉)) |
40 | | eleq1 2820 |
. . . . . 6
⊢ (𝑥 = ∩
∩ 𝐴 → (𝑥 ∈ 𝐵 ↔ ∩ ∩ 𝐴
∈ 𝐵)) |
41 | 40 | anbi1d 633 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝐴 → ((𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶) ↔ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
42 | 39, 41 | anbi12d 634 |
. . . 4
⊢ (𝑥 = ∩
∩ 𝐴 → ((𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
43 | 42 | ceqsexgv 3548 |
. . 3
⊢ (∩ ∩ 𝐴 ∈ V → (∃𝑥(𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
44 | 35, 37, 43 | pm5.21nii 383 |
. 2
⊢
(∃𝑥(𝑥 = ∩
∩ 𝐴 ∧ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
45 | 1, 32, 44 | 3bitri 300 |
1
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |