Step | Hyp | Ref
| Expression |
1 | | elxp7 5739 |
. 2
⊢ (A ∈ (B × 𝐶) ↔ (A ∈ (V × V)
∧ ((1st ‘A) ∈ B ∧ (2nd
‘A) ∈ 𝐶))) |
2 | | elvvuni 4347 |
. . . 4
⊢ (A ∈ (V × V)
→ ∪ A ∈ A) |
3 | 2 | adantr 261 |
. . 3
⊢
((A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶)) → ∪ A ∈ A) |
4 | | simprl 483 |
. . . . . 6
⊢ ((∪ A ∈ A ∧ (A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶))) → A ∈ (V ×
V)) |
5 | | eleq2 2098 |
. . . . . . . 8
⊢ (x = A →
(∪ A ∈ x ↔
∪ A ∈ A)) |
6 | | eleq1 2097 |
. . . . . . . . 9
⊢ (x = A →
(x ∈ (V
× V) ↔ A ∈ (V × V))) |
7 | | fveq2 5121 |
. . . . . . . . . . 11
⊢ (x = A →
(1st ‘x) = (1st
‘A)) |
8 | 7 | eleq1d 2103 |
. . . . . . . . . 10
⊢ (x = A →
((1st ‘x) ∈ B ↔
(1st ‘A) ∈ B)) |
9 | | fveq2 5121 |
. . . . . . . . . . 11
⊢ (x = A →
(2nd ‘x) = (2nd
‘A)) |
10 | 9 | eleq1d 2103 |
. . . . . . . . . 10
⊢ (x = A →
((2nd ‘x) ∈ 𝐶 ↔ (2nd ‘A) ∈ 𝐶)) |
11 | 8, 10 | anbi12d 442 |
. . . . . . . . 9
⊢ (x = A →
(((1st ‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶) ↔ ((1st
‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶))) |
12 | 6, 11 | anbi12d 442 |
. . . . . . . 8
⊢ (x = A →
((x ∈ (V
× V) ∧ ((1st ‘x) ∈ B ∧ (2nd
‘x) ∈ 𝐶)) ↔ (A ∈ (V × V)
∧ ((1st ‘A) ∈ B ∧ (2nd
‘A) ∈ 𝐶)))) |
13 | 5, 12 | anbi12d 442 |
. . . . . . 7
⊢ (x = A →
((∪ A ∈ x ∧ (x ∈ (V × V) ∧
((1st ‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶))) ↔ (∪ A ∈ A ∧ (A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶))))) |
14 | 13 | spcegv 2635 |
. . . . . 6
⊢ (A ∈ (V × V)
→ ((∪ A
∈ A ∧ (A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶))) → ∃x(∪ A ∈ x ∧ (x ∈ (V × V) ∧
((1st ‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶))))) |
15 | 4, 14 | mpcom 32 |
. . . . 5
⊢ ((∪ A ∈ A ∧ (A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶))) → ∃x(∪ A ∈ x ∧ (x ∈ (V × V) ∧
((1st ‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶)))) |
16 | | eluniab 3583 |
. . . . 5
⊢ (∪ A ∈ ∪ {x ∣ (x
∈ (V × V) ∧ ((1st ‘x) ∈ B ∧ (2nd
‘x) ∈ 𝐶))} ↔ ∃x(∪ A ∈ x ∧ (x ∈ (V × V) ∧
((1st ‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶)))) |
17 | 15, 16 | sylibr 137 |
. . . 4
⊢ ((∪ A ∈ A ∧ (A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶))) → ∪ A ∈ ∪ {x ∣ (x
∈ (V × V) ∧ ((1st ‘x) ∈ B ∧ (2nd
‘x) ∈ 𝐶))}) |
18 | | xp2 5741 |
. . . . . 6
⊢ (B × 𝐶) = {x
∈ (V × V) ∣ ((1st
‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶)} |
19 | | df-rab 2309 |
. . . . . 6
⊢ {x ∈ (V × V)
∣ ((1st ‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶)} = {x ∣ (x
∈ (V × V) ∧ ((1st ‘x) ∈ B ∧ (2nd
‘x) ∈ 𝐶))} |
20 | 18, 19 | eqtri 2057 |
. . . . 5
⊢ (B × 𝐶) = {x
∣ (x ∈ (V × V) ∧
((1st ‘x) ∈ B ∧ (2nd ‘x) ∈ 𝐶))} |
21 | 20 | unieqi 3581 |
. . . 4
⊢ ∪ (B × 𝐶) = ∪
{x ∣ (x ∈ (V × V)
∧ ((1st ‘x) ∈ B ∧ (2nd
‘x) ∈ 𝐶))} |
22 | 17, 21 | syl6eleqr 2128 |
. . 3
⊢ ((∪ A ∈ A ∧ (A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶))) → ∪ A ∈ ∪ (B × 𝐶)) |
23 | 3, 22 | mpancom 399 |
. 2
⊢
((A ∈ (V × V) ∧
((1st ‘A) ∈ B ∧ (2nd ‘A) ∈ 𝐶)) → ∪ A ∈ ∪ (B × 𝐶)) |
24 | 1, 23 | sylbi 114 |
1
⊢ (A ∈ (B × 𝐶) → ∪
A ∈ ∪ (B × 𝐶)) |