Step | Hyp | Ref
| Expression |
1 | | elxp 5365 |
. 2
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
2 | | sneq 4407 |
. . . . . . . . . . . 12
⊢ (𝐴 = 〈𝑥, 𝑦〉 → {𝐴} = {〈𝑥, 𝑦〉}) |
3 | 2 | rneqd 5585 |
. . . . . . . . . . 11
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ran {𝐴} = ran {〈𝑥, 𝑦〉}) |
4 | 3 | unieqd 4668 |
. . . . . . . . . 10
⊢ (𝐴 = 〈𝑥, 𝑦〉 → ∪
ran {𝐴} = ∪ ran {〈𝑥, 𝑦〉}) |
5 | | vex 3417 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ V |
6 | | vex 3417 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
7 | 5, 6 | op2nda 5862 |
. . . . . . . . . 10
⊢ ∪ ran {〈𝑥, 𝑦〉} = 𝑦 |
8 | 4, 7 | syl6req 2878 |
. . . . . . . . 9
⊢ (𝐴 = 〈𝑥, 𝑦〉 → 𝑦 = ∪ ran {𝐴}) |
9 | 8 | pm4.71ri 558 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑥, 𝑦〉 ↔ (𝑦 = ∪ ran {𝐴} ∧ 𝐴 = 〈𝑥, 𝑦〉)) |
10 | 9 | anbi1i 619 |
. . . . . . 7
⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ((𝑦 = ∪ ran {𝐴} ∧ 𝐴 = 〈𝑥, 𝑦〉) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) |
11 | | anass 462 |
. . . . . . 7
⊢ (((𝑦 = ∪
ran {𝐴} ∧ 𝐴 = 〈𝑥, 𝑦〉) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
12 | 10, 11 | bitri 267 |
. . . . . 6
⊢ ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑦 = ∪ ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
13 | 12 | exbii 1949 |
. . . . 5
⊢
(∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑦(𝑦 = ∪ ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)))) |
14 | | snex 5129 |
. . . . . . . 8
⊢ {𝐴} ∈ V |
15 | 14 | rnex 7362 |
. . . . . . 7
⊢ ran
{𝐴} ∈
V |
16 | 15 | uniex 7213 |
. . . . . 6
⊢ ∪ ran {𝐴} ∈ V |
17 | | opeq2 4624 |
. . . . . . . 8
⊢ (𝑦 = ∪
ran {𝐴} → 〈𝑥, 𝑦〉 = 〈𝑥, ∪ ran {𝐴}〉) |
18 | 17 | eqeq2d 2835 |
. . . . . . 7
⊢ (𝑦 = ∪
ran {𝐴} → (𝐴 = 〈𝑥, 𝑦〉 ↔ 𝐴 = 〈𝑥, ∪ ran {𝐴}〉)) |
19 | | eleq1 2894 |
. . . . . . . 8
⊢ (𝑦 = ∪
ran {𝐴} → (𝑦 ∈ 𝐶 ↔ ∪ ran
{𝐴} ∈ 𝐶)) |
20 | 19 | anbi2d 624 |
. . . . . . 7
⊢ (𝑦 = ∪
ran {𝐴} → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
21 | 18, 20 | anbi12d 626 |
. . . . . 6
⊢ (𝑦 = ∪
ran {𝐴} → ((𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
22 | 16, 21 | ceqsexv 3459 |
. . . . 5
⊢
(∃𝑦(𝑦 = ∪
ran {𝐴} ∧ (𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶))) ↔ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
23 | 13, 22 | bitri 267 |
. . . 4
⊢
(∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
24 | | inteq 4700 |
. . . . . . . 8
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 → ∩ 𝐴 =
∩ 〈𝑥, ∪ ran {𝐴}〉) |
25 | 24 | inteqd 4702 |
. . . . . . 7
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 → ∩ ∩ 𝐴 = ∩ ∩ 〈𝑥, ∪ ran {𝐴}〉) |
26 | 5, 16 | op1stb 5160 |
. . . . . . 7
⊢ ∩ ∩ 〈𝑥, ∪ ran {𝐴}〉 = 𝑥 |
27 | 25, 26 | syl6req 2878 |
. . . . . 6
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 → 𝑥 = ∩
∩ 𝐴) |
28 | 27 | pm4.71ri 558 |
. . . . 5
⊢ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ↔ (𝑥 = ∩
∩ 𝐴 ∧ 𝐴 = 〈𝑥, ∪ ran {𝐴}〉)) |
29 | 28 | anbi1i 619 |
. . . 4
⊢ ((𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ ((𝑥 = ∩ ∩ 𝐴
∧ 𝐴 = 〈𝑥, ∪
ran {𝐴}〉) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
30 | | anass 462 |
. . . 4
⊢ (((𝑥 = ∩
∩ 𝐴 ∧ 𝐴 = 〈𝑥, ∪ ran {𝐴}〉) ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
31 | 23, 29, 30 | 3bitri 289 |
. . 3
⊢
(∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
32 | 31 | exbii 1949 |
. 2
⊢
(∃𝑥∃𝑦(𝐴 = 〈𝑥, 𝑦〉 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ ∃𝑥(𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
33 | | eqvisset 3428 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝐴 → ∩ ∩ 𝐴
∈ V) |
34 | 33 | adantr 474 |
. . . 4
⊢ ((𝑥 = ∩
∩ 𝐴 ∧ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V) |
35 | 34 | exlimiv 2031 |
. . 3
⊢
(∃𝑥(𝑥 = ∩
∩ 𝐴 ∧ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) → ∩ ∩ 𝐴 ∈ V) |
36 | | elex 3429 |
. . . 4
⊢ (∩ ∩ 𝐴 ∈ 𝐵 → ∩ ∩ 𝐴
∈ V) |
37 | 36 | ad2antrl 721 |
. . 3
⊢ ((𝐴 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉 ∧ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) → ∩ ∩ 𝐴 ∈ V) |
38 | | opeq1 4623 |
. . . . . 6
⊢ (𝑥 = ∩
∩ 𝐴 → 〈𝑥, ∪ ran {𝐴}〉 = 〈∩ ∩ 𝐴, ∪ ran {𝐴}〉) |
39 | 38 | eqeq2d 2835 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝐴 → (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ↔ 𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉)) |
40 | | eleq1 2894 |
. . . . . 6
⊢ (𝑥 = ∩
∩ 𝐴 → (𝑥 ∈ 𝐵 ↔ ∩ ∩ 𝐴
∈ 𝐵)) |
41 | 40 | anbi1d 625 |
. . . . 5
⊢ (𝑥 = ∩
∩ 𝐴 → ((𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶) ↔ (∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
42 | 39, 41 | anbi12d 626 |
. . . 4
⊢ (𝑥 = ∩
∩ 𝐴 → ((𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
43 | 42 | ceqsexgv 3553 |
. . 3
⊢ (∩ ∩ 𝐴 ∈ V → (∃𝑥(𝑥 = ∩ ∩ 𝐴
∧ (𝐴 = 〈𝑥, ∪
ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
44 | 35, 37, 43 | pm5.21nii 370 |
. 2
⊢
(∃𝑥(𝑥 = ∩
∩ 𝐴 ∧ (𝐴 = 〈𝑥, ∪ ran {𝐴}〉 ∧ (𝑥 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
45 | 1, 32, 44 | 3bitri 289 |
1
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∩ ∩ 𝐴,
∪ ran {𝐴}〉 ∧ (∩
∩ 𝐴 ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |