| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . 5
⊢ ∪ 𝑈 =
∪ 𝑈 | 
| 2 |  | eqid 2737 | . . . . 5
⊢ (𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) | 
| 3 | 1, 2 | txcnmpt 23632 | . . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn (𝑅 ×t 𝑆))) | 
| 4 |  | uptx.1 | . . . . 5
⊢ 𝑇 = (𝑅 ×t 𝑆) | 
| 5 | 4 | oveq2i 7442 | . . . 4
⊢ (𝑈 Cn 𝑇) = (𝑈 Cn (𝑅 ×t 𝑆)) | 
| 6 | 3, 5 | eleqtrrdi 2852 | . . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇)) | 
| 7 |  | uptx.2 | . . . . . 6
⊢ 𝑋 = ∪
𝑅 | 
| 8 | 1, 7 | cnf 23254 | . . . . 5
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝐹:∪ 𝑈⟶𝑋) | 
| 9 |  | uptx.3 | . . . . . 6
⊢ 𝑌 = ∪
𝑆 | 
| 10 | 1, 9 | cnf 23254 | . . . . 5
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝐺:∪ 𝑈⟶𝑌) | 
| 11 |  | ffn 6736 | . . . . . . . 8
⊢ (𝐹:∪
𝑈⟶𝑋 → 𝐹 Fn ∪ 𝑈) | 
| 12 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐹 Fn ∪ 𝑈) | 
| 13 |  | fo1st 8034 | . . . . . . . . . 10
⊢
1st :V–onto→V | 
| 14 |  | fofn 6822 | . . . . . . . . . 10
⊢
(1st :V–onto→V → 1st Fn V) | 
| 15 | 13, 14 | ax-mp 5 | . . . . . . . . 9
⊢
1st Fn V | 
| 16 |  | ssv 4008 | . . . . . . . . 9
⊢ (𝑋 × 𝑌) ⊆ V | 
| 17 |  | fnssres 6691 | . . . . . . . . 9
⊢
((1st Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (1st ↾
(𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) | 
| 18 | 15, 16, 17 | mp2an 692 | . . . . . . . 8
⊢
(1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) | 
| 19 |  | ffvelcdm 7101 | . . . . . . . . . . . 12
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝑥 ∈ ∪ 𝑈) → (𝐹‘𝑥) ∈ 𝑋) | 
| 20 |  | ffvelcdm 7101 | . . . . . . . . . . . 12
⊢ ((𝐺:∪
𝑈⟶𝑌 ∧ 𝑥 ∈ ∪ 𝑈) → (𝐺‘𝑥) ∈ 𝑌) | 
| 21 |  | opelxpi 5722 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) ∈ 𝑋 ∧ (𝐺‘𝑥) ∈ 𝑌) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑋 × 𝑌)) | 
| 22 | 19, 20, 21 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝑥 ∈ ∪ 𝑈) ∧ (𝐺:∪ 𝑈⟶𝑌 ∧ 𝑥 ∈ ∪ 𝑈)) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑋 × 𝑌)) | 
| 23 | 22 | anandirs 679 | . . . . . . . . . 10
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑥 ∈ ∪ 𝑈) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝑋 × 𝑌)) | 
| 24 | 23 | fmpttd 7135 | . . . . . . . . 9
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌)) | 
| 25 |  | ffn 6736 | . . . . . . . . 9
⊢ ((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈) | 
| 26 | 24, 25 | syl 17 | . . . . . . . 8
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈) | 
| 27 | 24 | frnd 6744 | . . . . . . . 8
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ran (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝑋 × 𝑌)) | 
| 28 |  | fnco 6686 | . . . . . . . 8
⊢
(((1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈 ∧ ran (𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝑋 × 𝑌)) → ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) | 
| 29 | 18, 26, 27, 28 | mp3an2i 1468 | . . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) | 
| 30 |  | fvco3 7008 | . . . . . . . . 9
⊢ (((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((1st
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((1st ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) | 
| 31 | 24, 30 | sylan 580 | . . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((1st
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((1st ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) | 
| 32 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) | 
| 33 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) | 
| 34 | 32, 33 | opeq12d 4881 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) | 
| 35 |  | opex 5469 | . . . . . . . . . . 11
⊢
〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ V | 
| 36 | 34, 2, 35 | fvmpt 7016 | . . . . . . . . . 10
⊢ (𝑧 ∈ ∪ 𝑈
→ ((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) | 
| 37 | 36 | adantl 481 | . . . . . . . . 9
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) | 
| 38 | 37 | fveq2d 6910 | . . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((1st
↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧)) = ((1st ↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) | 
| 39 |  | ffvelcdm 7101 | . . . . . . . . . . . 12
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝑧 ∈ ∪ 𝑈) → (𝐹‘𝑧) ∈ 𝑋) | 
| 40 |  | ffvelcdm 7101 | . . . . . . . . . . . 12
⊢ ((𝐺:∪
𝑈⟶𝑌 ∧ 𝑧 ∈ ∪ 𝑈) → (𝐺‘𝑧) ∈ 𝑌) | 
| 41 |  | opelxpi 5722 | . . . . . . . . . . . 12
⊢ (((𝐹‘𝑧) ∈ 𝑋 ∧ (𝐺‘𝑧) ∈ 𝑌) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌)) | 
| 42 | 39, 40, 41 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝑧 ∈ ∪ 𝑈) ∧ (𝐺:∪ 𝑈⟶𝑌 ∧ 𝑧 ∈ ∪ 𝑈)) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌)) | 
| 43 | 42 | anandirs 679 | . . . . . . . . . 10
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝑋 × 𝑌)) | 
| 44 | 43 | fvresd 6926 | . . . . . . . . 9
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((1st
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (1st
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) | 
| 45 |  | fvex 6919 | . . . . . . . . . 10
⊢ (𝐹‘𝑧) ∈ V | 
| 46 |  | fvex 6919 | . . . . . . . . . 10
⊢ (𝐺‘𝑧) ∈ V | 
| 47 | 45, 46 | op1st 8022 | . . . . . . . . 9
⊢
(1st ‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐹‘𝑧) | 
| 48 | 44, 47 | eqtrdi 2793 | . . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((1st
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐹‘𝑧)) | 
| 49 | 31, 38, 48 | 3eqtrrd 2782 | . . . . . . 7
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (𝐹‘𝑧) = (((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧)) | 
| 50 | 12, 29, 49 | eqfnfvd 7054 | . . . . . 6
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐹 = ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 51 |  | uptx.5 | . . . . . . . 8
⊢ 𝑃 = (1st ↾ 𝑍) | 
| 52 |  | uptx.4 | . . . . . . . . 9
⊢ 𝑍 = (𝑋 × 𝑌) | 
| 53 | 52 | reseq2i 5994 | . . . . . . . 8
⊢
(1st ↾ 𝑍) = (1st ↾ (𝑋 × 𝑌)) | 
| 54 | 51, 53 | eqtri 2765 | . . . . . . 7
⊢ 𝑃 = (1st ↾
(𝑋 × 𝑌)) | 
| 55 | 54 | coeq1i 5870 | . . . . . 6
⊢ (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) = ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) | 
| 56 | 50, 55 | eqtr4di 2795 | . . . . 5
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 57 | 8, 10, 56 | syl2an 596 | . . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 58 |  | ffn 6736 | . . . . . . . 8
⊢ (𝐺:∪
𝑈⟶𝑌 → 𝐺 Fn ∪ 𝑈) | 
| 59 | 58 | adantl 481 | . . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐺 Fn ∪ 𝑈) | 
| 60 |  | fo2nd 8035 | . . . . . . . . . 10
⊢
2nd :V–onto→V | 
| 61 |  | fofn 6822 | . . . . . . . . . 10
⊢
(2nd :V–onto→V → 2nd Fn V) | 
| 62 | 60, 61 | ax-mp 5 | . . . . . . . . 9
⊢
2nd Fn V | 
| 63 |  | fnssres 6691 | . . . . . . . . 9
⊢
((2nd Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (2nd ↾
(𝑋 × 𝑌)) Fn (𝑋 × 𝑌)) | 
| 64 | 62, 16, 63 | mp2an 692 | . . . . . . . 8
⊢
(2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) | 
| 65 |  | fnco 6686 | . . . . . . . 8
⊢
(((2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn ∪
𝑈 ∧ ran (𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝑋 × 𝑌)) → ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) | 
| 66 | 64, 26, 27, 65 | mp3an2i 1468 | . . . . . . 7
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn ∪
𝑈) | 
| 67 |  | fvco3 7008 | . . . . . . . . 9
⊢ (((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((2nd
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((2nd ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) | 
| 68 | 24, 67 | sylan 580 | . . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (((2nd
↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((2nd ↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) | 
| 69 | 37 | fveq2d 6910 | . . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((2nd
↾ (𝑋 × 𝑌))‘((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧)) = ((2nd ↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) | 
| 70 | 43 | fvresd 6926 | . . . . . . . . 9
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((2nd
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (2nd
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) | 
| 71 | 45, 46 | op2nd 8023 | . . . . . . . . 9
⊢
(2nd ‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐺‘𝑧) | 
| 72 | 70, 71 | eqtrdi 2793 | . . . . . . . 8
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → ((2nd
↾ (𝑋 × 𝑌))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐺‘𝑧)) | 
| 73 | 68, 69, 72 | 3eqtrrd 2782 | . . . . . . 7
⊢ (((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) ∧ 𝑧 ∈ ∪ 𝑈) → (𝐺‘𝑧) = (((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧)) | 
| 74 | 59, 66, 73 | eqfnfvd 7054 | . . . . . 6
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐺 = ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 75 |  | uptx.6 | . . . . . . . 8
⊢ 𝑄 = (2nd ↾ 𝑍) | 
| 76 | 52 | reseq2i 5994 | . . . . . . . 8
⊢
(2nd ↾ 𝑍) = (2nd ↾ (𝑋 × 𝑌)) | 
| 77 | 75, 76 | eqtri 2765 | . . . . . . 7
⊢ 𝑄 = (2nd ↾
(𝑋 × 𝑌)) | 
| 78 | 77 | coeq1i 5870 | . . . . . 6
⊢ (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) = ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) | 
| 79 | 74, 78 | eqtr4di 2795 | . . . . 5
⊢ ((𝐹:∪
𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 80 | 8, 10, 79 | syl2an 596 | . . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 81 | 6, 57, 80 | jca32 515 | . . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))))) | 
| 82 |  | eleq1 2829 | . . . . 5
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (ℎ ∈ (𝑈 Cn 𝑇) ↔ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇))) | 
| 83 |  | coeq2 5869 | . . . . . . 7
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝑃 ∘ ℎ) = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 84 | 83 | eqeq2d 2748 | . . . . . 6
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝐹 = (𝑃 ∘ ℎ) ↔ 𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) | 
| 85 |  | coeq2 5869 | . . . . . . 7
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝑄 ∘ ℎ) = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) | 
| 86 | 85 | eqeq2d 2748 | . . . . . 6
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝐺 = (𝑄 ∘ ℎ) ↔ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) | 
| 87 | 84, 86 | anbi12d 632 | . . . . 5
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → ((𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))))) | 
| 88 | 82, 87 | anbi12d 632 | . . . 4
⊢ (ℎ = (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ↔ ((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))))) | 
| 89 | 88 | spcegv 3597 | . . 3
⊢ ((𝑥 ∈ ∪ 𝑈
↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) → (((𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ ∪ 𝑈 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) → ∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) | 
| 90 | 6, 81, 89 | sylc 65 | . 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) | 
| 91 |  | eqid 2737 | . . . . . . . 8
⊢ ∪ 𝑇 =
∪ 𝑇 | 
| 92 | 1, 91 | cnf 23254 | . . . . . . 7
⊢ (ℎ ∈ (𝑈 Cn 𝑇) → ℎ:∪ 𝑈⟶∪ 𝑇) | 
| 93 |  | cntop2 23249 | . . . . . . . . 9
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑅 ∈ Top) | 
| 94 |  | cntop2 23249 | . . . . . . . . 9
⊢ (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑆 ∈ Top) | 
| 95 | 4 | unieqi 4919 | . . . . . . . . . 10
⊢ ∪ 𝑇 =
∪ (𝑅 ×t 𝑆) | 
| 96 | 7, 9 | txuni 23600 | . . . . . . . . . 10
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆)) | 
| 97 | 95, 96 | eqtr4id 2796 | . . . . . . . . 9
⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∪ 𝑇 =
(𝑋 × 𝑌)) | 
| 98 | 93, 94, 97 | syl2an 596 | . . . . . . . 8
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∪ 𝑇 = (𝑋 × 𝑌)) | 
| 99 | 98 | feq3d 6723 | . . . . . . 7
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (ℎ:∪ 𝑈⟶∪ 𝑇
↔ ℎ:∪ 𝑈⟶(𝑋 × 𝑌))) | 
| 100 | 92, 99 | imbitrid 244 | . . . . . 6
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (ℎ ∈ (𝑈 Cn 𝑇) → ℎ:∪ 𝑈⟶(𝑋 × 𝑌))) | 
| 101 | 100 | anim1d 611 | . . . . 5
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) | 
| 102 |  | 3anass 1095 | . . . . 5
⊢ ((ℎ:∪
𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) | 
| 103 | 101, 102 | imbitrrdi 252 | . . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) | 
| 104 | 103 | alrimiv 1927 | . . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∀ℎ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) | 
| 105 |  | cntop1 23248 | . . . . . 6
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top) | 
| 106 | 105 | uniexd 7762 | . . . . 5
⊢ (𝐹 ∈ (𝑈 Cn 𝑅) → ∪ 𝑈 ∈ V) | 
| 107 | 54, 77 | upxp 23631 | . . . . 5
⊢ ((∪ 𝑈
∈ V ∧ 𝐹:∪ 𝑈⟶𝑋 ∧ 𝐺:∪ 𝑈⟶𝑌) → ∃!ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) | 
| 108 | 106, 8, 10, 107 | syl2an3an 1424 | . . . 4
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) | 
| 109 |  | eumo 2578 | . . . 4
⊢
(∃!ℎ(ℎ:∪
𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) | 
| 110 | 108, 109 | syl 17 | . . 3
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃*ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) | 
| 111 |  | moim 2544 | . . 3
⊢
(∀ℎ((ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (∃*ℎ(ℎ:∪ 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) | 
| 112 | 104, 110,
111 | sylc 65 | . 2
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) | 
| 113 |  | df-reu 3381 | . . 3
⊢
(∃!ℎ ∈
(𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ ∃!ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) | 
| 114 |  | df-eu 2569 | . . 3
⊢
(∃!ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ↔ (∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) | 
| 115 | 113, 114 | bitri 275 | . 2
⊢
(∃!ℎ ∈
(𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ (∃ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ ∃*ℎ(ℎ ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))))) | 
| 116 | 90, 112, 115 | sylanbrc 583 | 1
⊢ ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!ℎ ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |