Proof of Theorem funcnvtp
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simp1 1137 | . . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝐴 ∈ 𝑈) | 
| 2 |  | simp2 1138 | . . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → 𝐶 ∈ 𝑉) | 
| 3 |  | simp1 1137 | . . . 4
⊢ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) → 𝐵 ≠ 𝐷) | 
| 4 |  | funcnvpr 6628 | . . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) | 
| 5 | 1, 2, 3, 4 | syl2an3an 1424 | . . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) | 
| 6 |  | funcnvsn 6616 | . . . 4
⊢ Fun ◡{〈𝐸, 𝐹〉} | 
| 7 | 6 | a1i 11 | . . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{〈𝐸, 𝐹〉}) | 
| 8 |  | df-rn 5696 | . . . . . . 7
⊢ ran
{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} | 
| 9 |  | rnpropg 6242 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → ran {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐵, 𝐷}) | 
| 10 | 8, 9 | eqtr3id 2791 | . . . . . 6
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐵, 𝐷}) | 
| 11 | 10 | 3adant3 1133 | . . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐵, 𝐷}) | 
| 12 |  | df-rn 5696 | . . . . . . 7
⊢ ran
{〈𝐸, 𝐹〉} = dom ◡{〈𝐸, 𝐹〉} | 
| 13 |  | rnsnopg 6241 | . . . . . . 7
⊢ (𝐸 ∈ 𝑊 → ran {〈𝐸, 𝐹〉} = {𝐹}) | 
| 14 | 12, 13 | eqtr3id 2791 | . . . . . 6
⊢ (𝐸 ∈ 𝑊 → dom ◡{〈𝐸, 𝐹〉} = {𝐹}) | 
| 15 | 14 | 3ad2ant3 1136 | . . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → dom ◡{〈𝐸, 𝐹〉} = {𝐹}) | 
| 16 | 11, 15 | ineq12d 4221 | . . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) → (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉}) = ({𝐵, 𝐷} ∩ {𝐹})) | 
| 17 |  | disjprsn 4714 | . . . . 5
⊢ ((𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) → ({𝐵, 𝐷} ∩ {𝐹}) = ∅) | 
| 18 | 17 | 3adant1 1131 | . . . 4
⊢ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) → ({𝐵, 𝐷} ∩ {𝐹}) = ∅) | 
| 19 | 16, 18 | sylan9eq 2797 | . . 3
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉}) = ∅) | 
| 20 |  | funun 6612 | . . 3
⊢ (((Fun
◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∧ Fun ◡{〈𝐸, 𝐹〉}) ∧ (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉}) = ∅) → Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉})) | 
| 21 | 5, 7, 19, 20 | syl21anc 838 | . 2
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉})) | 
| 22 |  | df-tp 4631 | . . . . 5
⊢
{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = ({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉}) | 
| 23 | 22 | cnveqi 5885 | . . . 4
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = ◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉}) | 
| 24 |  | cnvun 6162 | . . . 4
⊢ ◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉}) = (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉}) | 
| 25 | 23, 24 | eqtri 2765 | . . 3
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} = (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉}) | 
| 26 | 25 | funeqi 6587 | . 2
⊢ (Fun
◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉} ↔ Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉})) | 
| 27 | 21, 26 | sylibr 234 | 1
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐸 ∈ 𝑊) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉, 〈𝐸, 𝐹〉}) |