Step |
Hyp |
Ref |
Expression |
1 |
|
txval.1 |
⊢ 𝐵 = ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) |
2 |
|
txuni2.1 |
⊢ 𝑋 = ∪ 𝑅 |
3 |
|
txuni2.2 |
⊢ 𝑌 = ∪ 𝑆 |
4 |
|
relxp |
⊢ Rel ( 𝑋 × 𝑌 ) |
5 |
2
|
eleq2i |
⊢ ( 𝑧 ∈ 𝑋 ↔ 𝑧 ∈ ∪ 𝑅 ) |
6 |
|
eluni2 |
⊢ ( 𝑧 ∈ ∪ 𝑅 ↔ ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 ) |
7 |
5 6
|
bitri |
⊢ ( 𝑧 ∈ 𝑋 ↔ ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 ) |
8 |
3
|
eleq2i |
⊢ ( 𝑤 ∈ 𝑌 ↔ 𝑤 ∈ ∪ 𝑆 ) |
9 |
|
eluni2 |
⊢ ( 𝑤 ∈ ∪ 𝑆 ↔ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 ) |
10 |
8 9
|
bitri |
⊢ ( 𝑤 ∈ 𝑌 ↔ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 ) |
11 |
7 10
|
anbi12i |
⊢ ( ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ↔ ( ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 ∧ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 ) ) |
12 |
|
opelxp |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝑋 × 𝑌 ) ↔ ( 𝑧 ∈ 𝑋 ∧ 𝑤 ∈ 𝑌 ) ) |
13 |
|
reeanv |
⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) ↔ ( ∃ 𝑟 ∈ 𝑅 𝑧 ∈ 𝑟 ∧ ∃ 𝑠 ∈ 𝑆 𝑤 ∈ 𝑠 ) ) |
14 |
11 12 13
|
3bitr4i |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝑋 × 𝑌 ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) ) |
15 |
|
opelxp |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝑟 × 𝑠 ) ↔ ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) ) |
16 |
|
eqid |
⊢ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑠 ) |
17 |
|
xpeq1 |
⊢ ( 𝑥 = 𝑟 → ( 𝑥 × 𝑦 ) = ( 𝑟 × 𝑦 ) ) |
18 |
17
|
eqeq2d |
⊢ ( 𝑥 = 𝑟 → ( ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ↔ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑦 ) ) ) |
19 |
|
xpeq2 |
⊢ ( 𝑦 = 𝑠 → ( 𝑟 × 𝑦 ) = ( 𝑟 × 𝑠 ) ) |
20 |
19
|
eqeq2d |
⊢ ( 𝑦 = 𝑠 → ( ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑦 ) ↔ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑠 ) ) ) |
21 |
18 20
|
rspc2ev |
⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ∧ ( 𝑟 × 𝑠 ) = ( 𝑟 × 𝑠 ) ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ) |
22 |
16 21
|
mp3an3 |
⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ) |
23 |
|
vex |
⊢ 𝑟 ∈ V |
24 |
|
vex |
⊢ 𝑠 ∈ V |
25 |
23 24
|
xpex |
⊢ ( 𝑟 × 𝑠 ) ∈ V |
26 |
|
eqeq1 |
⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( 𝑧 = ( 𝑥 × 𝑦 ) ↔ ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ) ) |
27 |
26
|
2rexbidv |
⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 𝑧 = ( 𝑥 × 𝑦 ) ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ) ) |
28 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) |
29 |
28
|
rnmpo |
⊢ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) = { 𝑧 ∣ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 𝑧 = ( 𝑥 × 𝑦 ) } |
30 |
1 29
|
eqtri |
⊢ 𝐵 = { 𝑧 ∣ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 𝑧 = ( 𝑥 × 𝑦 ) } |
31 |
25 27 30
|
elab2 |
⊢ ( ( 𝑟 × 𝑠 ) ∈ 𝐵 ↔ ∃ 𝑥 ∈ 𝑅 ∃ 𝑦 ∈ 𝑆 ( 𝑟 × 𝑠 ) = ( 𝑥 × 𝑦 ) ) |
32 |
22 31
|
sylibr |
⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑟 × 𝑠 ) ∈ 𝐵 ) |
33 |
|
elssuni |
⊢ ( ( 𝑟 × 𝑠 ) ∈ 𝐵 → ( 𝑟 × 𝑠 ) ⊆ ∪ 𝐵 ) |
34 |
32 33
|
syl |
⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( 𝑟 × 𝑠 ) ⊆ ∪ 𝐵 ) |
35 |
34
|
sseld |
⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝑟 × 𝑠 ) → 〈 𝑧 , 𝑤 〉 ∈ ∪ 𝐵 ) ) |
36 |
15 35
|
syl5bir |
⊢ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) → ( ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) → 〈 𝑧 , 𝑤 〉 ∈ ∪ 𝐵 ) ) |
37 |
36
|
rexlimivv |
⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ 𝑟 ∧ 𝑤 ∈ 𝑠 ) → 〈 𝑧 , 𝑤 〉 ∈ ∪ 𝐵 ) |
38 |
14 37
|
sylbi |
⊢ ( 〈 𝑧 , 𝑤 〉 ∈ ( 𝑋 × 𝑌 ) → 〈 𝑧 , 𝑤 〉 ∈ ∪ 𝐵 ) |
39 |
4 38
|
relssi |
⊢ ( 𝑋 × 𝑌 ) ⊆ ∪ 𝐵 |
40 |
|
elssuni |
⊢ ( 𝑥 ∈ 𝑅 → 𝑥 ⊆ ∪ 𝑅 ) |
41 |
40 2
|
sseqtrrdi |
⊢ ( 𝑥 ∈ 𝑅 → 𝑥 ⊆ 𝑋 ) |
42 |
|
elssuni |
⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ⊆ ∪ 𝑆 ) |
43 |
42 3
|
sseqtrrdi |
⊢ ( 𝑦 ∈ 𝑆 → 𝑦 ⊆ 𝑌 ) |
44 |
|
xpss12 |
⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌 ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) ) |
45 |
41 43 44
|
syl2an |
⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) ) |
46 |
|
vex |
⊢ 𝑥 ∈ V |
47 |
|
vex |
⊢ 𝑦 ∈ V |
48 |
46 47
|
xpex |
⊢ ( 𝑥 × 𝑦 ) ∈ V |
49 |
48
|
elpw |
⊢ ( ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 ) ↔ ( 𝑥 × 𝑦 ) ⊆ ( 𝑋 × 𝑌 ) ) |
50 |
45 49
|
sylibr |
⊢ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 ) ) |
51 |
50
|
rgen2 |
⊢ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 ) |
52 |
28
|
fmpo |
⊢ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑆 ( 𝑥 × 𝑦 ) ∈ 𝒫 ( 𝑋 × 𝑌 ) ↔ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑅 × 𝑆 ) ⟶ 𝒫 ( 𝑋 × 𝑌 ) ) |
53 |
51 52
|
mpbi |
⊢ ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑅 × 𝑆 ) ⟶ 𝒫 ( 𝑋 × 𝑌 ) |
54 |
|
frn |
⊢ ( ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) : ( 𝑅 × 𝑆 ) ⟶ 𝒫 ( 𝑋 × 𝑌 ) → ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( 𝑋 × 𝑌 ) ) |
55 |
53 54
|
ax-mp |
⊢ ran ( 𝑥 ∈ 𝑅 , 𝑦 ∈ 𝑆 ↦ ( 𝑥 × 𝑦 ) ) ⊆ 𝒫 ( 𝑋 × 𝑌 ) |
56 |
1 55
|
eqsstri |
⊢ 𝐵 ⊆ 𝒫 ( 𝑋 × 𝑌 ) |
57 |
|
sspwuni |
⊢ ( 𝐵 ⊆ 𝒫 ( 𝑋 × 𝑌 ) ↔ ∪ 𝐵 ⊆ ( 𝑋 × 𝑌 ) ) |
58 |
56 57
|
mpbi |
⊢ ∪ 𝐵 ⊆ ( 𝑋 × 𝑌 ) |
59 |
39 58
|
eqssi |
⊢ ( 𝑋 × 𝑌 ) = ∪ 𝐵 |