Step |
Hyp |
Ref |
Expression |
1 |
|
distop |
⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ Top ) |
2 |
|
distop |
⊢ ( 𝐵 ∈ 𝑊 → 𝒫 𝐵 ∈ Top ) |
3 |
|
unipw |
⊢ ∪ 𝒫 𝐴 = 𝐴 |
4 |
3
|
eqcomi |
⊢ 𝐴 = ∪ 𝒫 𝐴 |
5 |
|
unipw |
⊢ ∪ 𝒫 𝐵 = 𝐵 |
6 |
5
|
eqcomi |
⊢ 𝐵 = ∪ 𝒫 𝐵 |
7 |
4 6
|
txuni |
⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐵 ∈ Top ) → ( 𝐴 × 𝐵 ) = ∪ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ) |
8 |
1 2 7
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × 𝐵 ) = ∪ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ) |
9 |
|
eqimss2 |
⊢ ( ( 𝐴 × 𝐵 ) = ∪ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) → ∪ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) ) |
10 |
8 9
|
syl |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) ) |
11 |
|
sspwuni |
⊢ ( ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 × 𝐵 ) ↔ ∪ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) ) |
12 |
10 11
|
sylibr |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ⊆ 𝒫 ( 𝐴 × 𝐵 ) ) |
13 |
|
elelpwi |
⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) → 𝑦 ∈ ( 𝐴 × 𝐵 ) ) |
14 |
13
|
adantl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ ( 𝐴 × 𝐵 ) ) |
15 |
|
xp1st |
⊢ ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → ( 1st ‘ 𝑦 ) ∈ 𝐴 ) |
16 |
|
snelpwi |
⊢ ( ( 1st ‘ 𝑦 ) ∈ 𝐴 → { ( 1st ‘ 𝑦 ) } ∈ 𝒫 𝐴 ) |
17 |
14 15 16
|
3syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ( 1st ‘ 𝑦 ) } ∈ 𝒫 𝐴 ) |
18 |
|
xp2nd |
⊢ ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → ( 2nd ‘ 𝑦 ) ∈ 𝐵 ) |
19 |
|
snelpwi |
⊢ ( ( 2nd ‘ 𝑦 ) ∈ 𝐵 → { ( 2nd ‘ 𝑦 ) } ∈ 𝒫 𝐵 ) |
20 |
14 18 19
|
3syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { ( 2nd ‘ 𝑦 ) } ∈ 𝒫 𝐵 ) |
21 |
|
vsnid |
⊢ 𝑦 ∈ { 𝑦 } |
22 |
|
1st2nd2 |
⊢ ( 𝑦 ∈ ( 𝐴 × 𝐵 ) → 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ) |
23 |
14 22
|
syl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 = 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ) |
24 |
23
|
sneqd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { 𝑦 } = { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ) |
25 |
21 24
|
eleqtrid |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ) |
26 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 𝑦 ∈ 𝑥 ) |
27 |
23 26
|
eqeltrrd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 ∈ 𝑥 ) |
28 |
27
|
snssd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ⊆ 𝑥 ) |
29 |
|
xpeq1 |
⊢ ( 𝑧 = { ( 1st ‘ 𝑦 ) } → ( 𝑧 × 𝑤 ) = ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ) |
30 |
29
|
eleq2d |
⊢ ( 𝑧 = { ( 1st ‘ 𝑦 ) } → ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ↔ 𝑦 ∈ ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ) ) |
31 |
29
|
sseq1d |
⊢ ( 𝑧 = { ( 1st ‘ 𝑦 ) } → ( ( 𝑧 × 𝑤 ) ⊆ 𝑥 ↔ ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) ) |
32 |
30 31
|
anbi12d |
⊢ ( 𝑧 = { ( 1st ‘ 𝑦 ) } → ( ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ∧ ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) ) ) |
33 |
|
xpeq2 |
⊢ ( 𝑤 = { ( 2nd ‘ 𝑦 ) } → ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) = ( { ( 1st ‘ 𝑦 ) } × { ( 2nd ‘ 𝑦 ) } ) ) |
34 |
|
fvex |
⊢ ( 1st ‘ 𝑦 ) ∈ V |
35 |
|
fvex |
⊢ ( 2nd ‘ 𝑦 ) ∈ V |
36 |
34 35
|
xpsn |
⊢ ( { ( 1st ‘ 𝑦 ) } × { ( 2nd ‘ 𝑦 ) } ) = { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } |
37 |
33 36
|
eqtrdi |
⊢ ( 𝑤 = { ( 2nd ‘ 𝑦 ) } → ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) = { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ) |
38 |
37
|
eleq2d |
⊢ ( 𝑤 = { ( 2nd ‘ 𝑦 ) } → ( 𝑦 ∈ ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ↔ 𝑦 ∈ { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ) ) |
39 |
37
|
sseq1d |
⊢ ( 𝑤 = { ( 2nd ‘ 𝑦 ) } → ( ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ↔ { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ⊆ 𝑥 ) ) |
40 |
38 39
|
anbi12d |
⊢ ( 𝑤 = { ( 2nd ‘ 𝑦 ) } → ( ( 𝑦 ∈ ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ∧ ( { ( 1st ‘ 𝑦 ) } × 𝑤 ) ⊆ 𝑥 ) ↔ ( 𝑦 ∈ { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ∧ { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ⊆ 𝑥 ) ) ) |
41 |
32 40
|
rspc2ev |
⊢ ( ( { ( 1st ‘ 𝑦 ) } ∈ 𝒫 𝐴 ∧ { ( 2nd ‘ 𝑦 ) } ∈ 𝒫 𝐵 ∧ ( 𝑦 ∈ { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ∧ { 〈 ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) 〉 } ⊆ 𝑥 ) ) → ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) |
42 |
17 20 25 28 41
|
syl112anc |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ) ) → ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) |
43 |
42
|
expr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) ) |
44 |
43
|
ralrimdva |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) ) |
45 |
|
eltx |
⊢ ( ( 𝒫 𝐴 ∈ Top ∧ 𝒫 𝐵 ∈ Top ) → ( 𝑥 ∈ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) ) |
46 |
1 2 45
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ 𝒫 𝐴 ∃ 𝑤 ∈ 𝒫 𝐵 ( 𝑦 ∈ ( 𝑧 × 𝑤 ) ∧ ( 𝑧 × 𝑤 ) ⊆ 𝑥 ) ) ) |
47 |
44 46
|
sylibrd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) → 𝑥 ∈ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ) ) |
48 |
47
|
ssrdv |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝒫 ( 𝐴 × 𝐵 ) ⊆ ( 𝒫 𝐴 ×t 𝒫 𝐵 ) ) |
49 |
12 48
|
eqssd |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝒫 𝐴 ×t 𝒫 𝐵 ) = 𝒫 ( 𝐴 × 𝐵 ) ) |