Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . 5
⊢ ∪ 𝑈 =
∪ 𝑈 |
2 | | eqid 2610 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
3 | 1, 2 | txcnmpt 21237 |
. . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn (𝑅 ×t 𝑆))) |
4 | | uptx.1 |
. . . . 5
⊢ 𝑇 = (𝑅 ×t 𝑆) |
5 | 4 | oveq2i 6560 |
. . . 4
⊢ (𝑈 Cn 𝑇) = (𝑈 Cn (𝑅 ×t 𝑆)) |
6 | 3, 5 | syl6eleqr 2699 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇)) |
7 | | uptx.2 |
. . . . . 6
⊢ 𝑋 = ∪
𝑅 |
8 | 1, 7 | cnf 20860 |
. . . . 5
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝐹:∪ 𝑈⟶𝑋) |
9 | | uptx.3 |
. . . . . 6
⊢ 𝑌 = ∪
𝑆 |
10 | 1, 9 | cnf 20860 |
. . . . 5
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝐺:∪ 𝑈⟶𝑌) |
11 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:∪
𝑈⟶𝑋 → 𝐹 Fn ∪ 𝑈) |
12 | 11 | adantr 480 |
. . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐹 Fn ∪ 𝑈) |
13 | | fo1st 7079 |
. . . . . . . . . . 11
⊢
1st :V–onto→V |
14 | | fofn 6030 |
. . . . . . . . . . 11
⊢
(1st :V–onto→V → 1st Fn V) |
15 | 13, 14 | ax-mp 5 |
. . . . . . . . . 10
⊢
1st Fn V |
16 | | ssv 3588 |
. . . . . . . . . 10
⊢ (𝑋 × 𝑌) ⊆ V |
17 | | fnssres 5918 |
. . . . . . . . . 10
⊢
((1st Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (1st ↾
(𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
18 | 15, 16, 17 | mp2an 704 |
. . . . . . . . 9
⊢
(1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → (1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
20 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝑥 ∈ ∪ 𝑈) → (𝐹‘𝑥) ∈ 𝑋) |
21 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐺:∪
𝑈⟶𝑌 ∧ 𝑥 ∈ ∪ 𝑈) → (𝐺‘𝑥) ∈ 𝑌) |
22 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) ∈ 𝑋 ∧ (𝐺‘𝑥) ∈ 𝑌) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑋 × 𝑌)) |
23 | 20, 21, 22 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝑥 ∈ ∪ 𝑈) ∧ (𝐺:∪ 𝑈⟶𝑌 ∧ 𝑥 ∈ ∪ 𝑈)) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑋 × 𝑌)) |
24 | 23 | anandirs 870 |
. . . . . . . . . 10
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑥 ∈ ∪ 𝑈) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑋 × 𝑌)) |
25 | 24, 2 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌)) |
26 | | ffn 5958 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈) |
28 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌) → ran (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝑋 × 𝑌)) |
29 | 25, 28 | syl 17 |
. . . . . . . 8
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ran (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝑋 × 𝑌)) |
30 | | fnco 5913 |
. . . . . . . 8
⊢
(((1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈 ∧ ran (𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝑋 × 𝑌)) → ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) |
31 | 19, 27, 29, 30 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) |
32 | | fvco3 6185 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((1st
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((1st ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
33 | 25, 32 | sylan 487 |
. . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((1st
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((1st ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
34 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
35 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
36 | 34, 35 | opeq12d 4348 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
37 | | opex 4859 |
. . . . . . . . . . 11
⊢
〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ V |
38 | 36, 2, 37 | fvmpt 6191 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ∪ 𝑈
→ ((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
39 | 38 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
40 | 39 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((1st
↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧)) = ((1st ↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
41 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝑧 ∈ ∪ 𝑈) → (𝐹‘𝑧) ∈ 𝑋) |
42 | | ffvelrn 6265 |
. . . . . . . . . . . 12
⊢ ((𝐺:∪
𝑈⟶𝑌 ∧ 𝑧 ∈ ∪ 𝑈) → (𝐺‘𝑧) ∈ 𝑌) |
43 | | opelxpi 5072 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ 𝑋 ∧ (𝐺‘𝑧) ∈ 𝑌) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌)) |
44 | 41, 42, 43 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝑧 ∈ ∪ 𝑈) ∧ (𝐺:∪ 𝑈⟶𝑌 ∧ 𝑧 ∈ ∪ 𝑈)) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌)) |
45 | 44 | anandirs 870 |
. . . . . . . . . 10
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌)) |
46 | | fvres 6117 |
. . . . . . . . . 10
⊢
(〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌) → ((1st ↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (1st
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
47 | 45, 46 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((1st
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (1st
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
48 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐹‘𝑧) ∈ V |
49 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐺‘𝑧) ∈ V |
50 | 48, 49 | op1st 7067 |
. . . . . . . . 9
⊢
(1st ‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐹‘𝑧) |
51 | 47, 50 | syl6eq 2660 |
. . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((1st
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐹‘𝑧)) |
52 | 33, 40, 51 | 3eqtrrd 2649 |
. . . . . . 7
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (𝐹‘𝑧) = (((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧)) |
53 | 12, 31, 52 | eqfnfvd 6222 |
. . . . . 6
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐹 = ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
54 | | uptx.5 |
. . . . . . . 8
⊢ 𝑃 = (1st ↾ 𝑍) |
55 | | uptx.4 |
. . . . . . . . 9
⊢ 𝑍 = (𝑋 × 𝑌) |
56 | 55 | reseq2i 5314 |
. . . . . . . 8
⊢
(1st ↾ 𝑍) = (1st ↾ (𝑋 × 𝑌)) |
57 | 54, 56 | eqtri 2632 |
. . . . . . 7
⊢ 𝑃 = (1st ↾
(𝑋 × 𝑌)) |
58 | 57 | coeq1i 5203 |
. . . . . 6
⊢ (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) = ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
59 | 53, 58 | syl6eqr 2662 |
. . . . 5
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
60 | 8, 10, 59 | syl2an 493 |
. . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
61 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐺:∪
𝑈⟶𝑌 → 𝐺 Fn ∪ 𝑈) |
62 | 61 | adantl 481 |
. . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐺 Fn ∪ 𝑈) |
63 | | fo2nd 7080 |
. . . . . . . . . . 11
⊢
2nd :V–onto→V |
64 | | fofn 6030 |
. . . . . . . . . . 11
⊢
(2nd :V–onto→V → 2nd Fn V) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . 10
⊢
2nd Fn V |
66 | | fnssres 5918 |
. . . . . . . . . 10
⊢
((2nd Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (2nd ↾
(𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
67 | 65, 16, 66 | mp2an 704 |
. . . . . . . . 9
⊢
(2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) |
68 | 67 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) |
69 | | fnco 5913 |
. . . . . . . 8
⊢
(((2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈 ∧ ran (𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝑋 × 𝑌)) → ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) |
70 | 68, 27, 29, 69 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) |
71 | | fvco3 6185 |
. . . . . . . . 9
⊢ (((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((2nd
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((2nd ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
72 | 25, 71 | sylan 487 |
. . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((2nd
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((2nd ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
73 | 39 | fveq2d 6107 |
. . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((2nd
↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧)) = ((2nd ↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
74 | | fvres 6117 |
. . . . . . . . . 10
⊢
(〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌) → ((2nd ↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (2nd
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
75 | 45, 74 | syl 17 |
. . . . . . . . 9
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((2nd
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (2nd
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
76 | 48, 49 | op2nd 7068 |
. . . . . . . . 9
⊢
(2nd ‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐺‘𝑧) |
77 | 75, 76 | syl6eq 2660 |
. . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((2nd
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐺‘𝑧)) |
78 | 72, 73, 77 | 3eqtrrd 2649 |
. . . . . . 7
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (𝐺‘𝑧) = (((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧)) |
79 | 62, 70, 78 | eqfnfvd 6222 |
. . . . . 6
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐺 = ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
80 | | uptx.6 |
. . . . . . . 8
⊢ 𝑄 = (2nd ↾ 𝑍) |
81 | 55 | reseq2i 5314 |
. . . . . . . 8
⊢
(2nd ↾ 𝑍) = (2nd ↾ (𝑋 × 𝑌)) |
82 | 80, 81 | eqtri 2632 |
. . . . . . 7
⊢ 𝑄 = (2nd ↾
(𝑋 × 𝑌)) |
83 | 82 | coeq1i 5203 |
. . . . . 6
⊢ (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) = ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
84 | 79, 83 | syl6eqr 2662 |
. . . . 5
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
85 | 8, 10, 84 | syl2an 493 |
. . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
86 | 6, 60, 85 | jca32 556 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))))) |
87 | | eleq1 2676 |
. . . . 5
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (ℎ ∈ (𝑈 Cn 𝑇) ↔ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇))) |
88 | | coeq2 5202 |
. . . . . . 7
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝑃 ∘ ℎ) = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
89 | 88 | eqeq2d 2620 |
. . . . . 6
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝐹 = (𝑃 ∘ ℎ) ↔ 𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) |
90 | | coeq2 5202 |
. . . . . . 7
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝑄 ∘ ℎ) = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
91 | 90 | eqeq2d 2620 |
. . . . . 6
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝐺 = (𝑄 ∘ ℎ) ↔ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) |
92 | 89, 91 | anbi12d 743 |
. . . . 5
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → ((𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))))) |
93 | 87, 92 | anbi12d 743 |
. . . 4
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ↔ ((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))))) |
94 | 93 | spcegv 3267 |
. . 3
⊢ ((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) → (((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) → ∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) |
95 | 6, 86, 94 | sylc 63 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) |
96 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝑇 =
∪ 𝑇 |
97 | 1, 96 | cnf 20860 |
. . . . . . 7
⊢ (ℎ ∈ (𝑈 Cn 𝑇) → ℎ:∪ 𝑈⟶∪ 𝑇) |
98 | | cntop2 20855 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑅 ∈ Top) |
99 | | cntop2 20855 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑆 ∈ Top) |
100 | 7, 9 | txuni 21205 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) |
101 | 4 | unieqi 4381 |
. . . . . . . . . 10
⊢ ∪ 𝑇 =
∪ (𝑅 ×t 𝑆) |
102 | 100, 101 | syl6reqr 2663 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ 𝑇 =
(𝑋 × 𝑌)) |
103 | 98, 99, 102 | syl2an 493 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∪ 𝑇 = (𝑋 × 𝑌)) |
104 | 103 | feq3d 5945 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (ℎ:∪ 𝑈⟶∪ 𝑇
↔ ℎ:∪ 𝑈⟶(𝑋 × 𝑌))) |
105 | 97, 104 | syl5ib 233 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (ℎ ∈ (𝑈 Cn 𝑇) → ℎ:∪ 𝑈⟶(𝑋 × 𝑌))) |
106 | 105 | anim1d 586 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) |
107 | | 3anass 1035 |
. . . . 5
⊢ ((ℎ:∪
𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) |
108 | 106, 107 | syl6ibr 241 |
. . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) |
109 | 108 | alrimiv 1842 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∀ℎ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) |
110 | | cntop1 20854 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top) |
111 | | uniexg 6853 |
. . . . . . 7
⊢ (𝑈 ∈ Top → ∪ 𝑈
∈ V) |
112 | 110, 111 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → ∪ 𝑈 ∈ V) |
113 | 112 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∪ 𝑈 ∈ V) |
114 | 8 | adantr 480 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐹:∪ 𝑈⟶𝑋) |
115 | 10 | adantl 481 |
. . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐺:∪ 𝑈⟶𝑌) |
116 | 57, 82 | upxp 21236 |
. . . . 5
⊢ ((∪ 𝑈
∈ V ∧ 𝐹:∪ 𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ∃!ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |
117 | 113, 114,
115, 116 | syl3anc 1318 |
. . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |
118 | | eumo 2487 |
. . . 4
⊢
(∃!ℎ(ℎ:∪
𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |
119 | 117, 118 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃*ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |
120 | | moim 2507 |
. . 3
⊢
(∀ℎ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (∃*ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) |
121 | 109, 119,
120 | sylc 63 |
. 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) |
122 | | df-reu 2903 |
. . 3
⊢
(∃!ℎ ∈
(𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) |
123 | | eu5 2484 |
. . 3
⊢
(∃!ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ↔ (∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) |
124 | 122, 123 | bitri 263 |
. 2
⊢
(∃!ℎ ∈
(𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ (∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) |
125 | 95, 121, 124 | sylanbrc 695 |
1
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |