Proof of Theorem funtpg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 3simpa 1148 | . . . 4
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉)) | 
| 2 |  | 3simpa 1148 | . . . 4
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺)) | 
| 3 |  | simp1 1136 | . . . 4
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → 𝑋 ≠ 𝑌) | 
| 4 |  | funprg 6619 | . . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺) ∧ 𝑋 ≠ 𝑌) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}) | 
| 5 | 1, 2, 3, 4 | syl3an 1160 | . . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉}) | 
| 6 |  | simp3 1138 | . . . . 5
⊢ ((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) → 𝑍 ∈ 𝑊) | 
| 7 |  | simp3 1138 | . . . . 5
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → 𝐶 ∈ 𝐻) | 
| 8 |  | funsng 6616 | . . . . 5
⊢ ((𝑍 ∈ 𝑊 ∧ 𝐶 ∈ 𝐻) → Fun {〈𝑍, 𝐶〉}) | 
| 9 | 6, 7, 8 | syl2an 596 | . . . 4
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻)) → Fun {〈𝑍, 𝐶〉}) | 
| 10 | 9 | 3adant3 1132 | . . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑍, 𝐶〉}) | 
| 11 |  | dmpropg 6234 | . . . . . . 7
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺) → dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} = {𝑋, 𝑌}) | 
| 12 |  | dmsnopg 6232 | . . . . . . 7
⊢ (𝐶 ∈ 𝐻 → dom {〈𝑍, 𝐶〉} = {𝑍}) | 
| 13 | 11, 12 | ineqan12d 4221 | . . . . . 6
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺) ∧ 𝐶 ∈ 𝐻) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ({𝑋, 𝑌} ∩ {𝑍})) | 
| 14 | 13 | 3impa 1109 | . . . . 5
⊢ ((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ({𝑋, 𝑌} ∩ {𝑍})) | 
| 15 |  | disjprsn 4713 | . . . . . 6
⊢ ((𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅) | 
| 16 | 15 | 3adant1 1130 | . . . . 5
⊢ ((𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍) → ({𝑋, 𝑌} ∩ {𝑍}) = ∅) | 
| 17 | 14, 16 | sylan9eq 2796 | . . . 4
⊢ (((𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ∅) | 
| 18 | 17 | 3adant1 1130 | . . 3
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ∅) | 
| 19 |  | funun 6611 | . . 3
⊢ (((Fun
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∧ Fun {〈𝑍, 𝐶〉}) ∧ (dom {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∩ dom {〈𝑍, 𝐶〉}) = ∅) → Fun ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉})) | 
| 20 | 5, 10, 18, 19 | syl21anc 837 | . 2
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉})) | 
| 21 |  | df-tp 4630 | . . 3
⊢
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} = ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉}) | 
| 22 | 21 | funeqi 6586 | . 2
⊢ (Fun
{〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉} ↔ Fun ({〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉} ∪ {〈𝑍, 𝐶〉})) | 
| 23 | 20, 22 | sylibr 234 | 1
⊢ (((𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑊) ∧ (𝐴 ∈ 𝐹 ∧ 𝐵 ∈ 𝐺 ∧ 𝐶 ∈ 𝐻) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → Fun {〈𝑋, 𝐴〉, 〈𝑌, 𝐵〉, 〈𝑍, 𝐶〉}) |