Proof of Theorem funcnvpr
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | funcnvsn 6616 | . . . 4
⊢ Fun ◡{〈𝐴, 𝐵〉} | 
| 2 |  | funcnvsn 6616 | . . . 4
⊢ Fun ◡{〈𝐶, 𝐷〉} | 
| 3 | 1, 2 | pm3.2i 470 | . . 3
⊢ (Fun
◡{〈𝐴, 𝐵〉} ∧ Fun ◡{〈𝐶, 𝐷〉}) | 
| 4 |  | df-rn 5696 | . . . . . . 7
⊢ ran
{〈𝐴, 𝐵〉} = dom ◡{〈𝐴, 𝐵〉} | 
| 5 |  | rnsnopg 6241 | . . . . . . 7
⊢ (𝐴 ∈ 𝑈 → ran {〈𝐴, 𝐵〉} = {𝐵}) | 
| 6 | 4, 5 | eqtr3id 2791 | . . . . . 6
⊢ (𝐴 ∈ 𝑈 → dom ◡{〈𝐴, 𝐵〉} = {𝐵}) | 
| 7 |  | df-rn 5696 | . . . . . . 7
⊢ ran
{〈𝐶, 𝐷〉} = dom ◡{〈𝐶, 𝐷〉} | 
| 8 |  | rnsnopg 6241 | . . . . . . 7
⊢ (𝐶 ∈ 𝑉 → ran {〈𝐶, 𝐷〉} = {𝐷}) | 
| 9 | 7, 8 | eqtr3id 2791 | . . . . . 6
⊢ (𝐶 ∈ 𝑉 → dom ◡{〈𝐶, 𝐷〉} = {𝐷}) | 
| 10 | 6, 9 | ineqan12d 4222 | . . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → (dom ◡{〈𝐴, 𝐵〉} ∩ dom ◡{〈𝐶, 𝐷〉}) = ({𝐵} ∩ {𝐷})) | 
| 11 | 10 | 3adant3 1133 | . . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → (dom ◡{〈𝐴, 𝐵〉} ∩ dom ◡{〈𝐶, 𝐷〉}) = ({𝐵} ∩ {𝐷})) | 
| 12 |  | disjsn2 4712 | . . . . 5
⊢ (𝐵 ≠ 𝐷 → ({𝐵} ∩ {𝐷}) = ∅) | 
| 13 | 12 | 3ad2ant3 1136 | . . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → ({𝐵} ∩ {𝐷}) = ∅) | 
| 14 | 11, 13 | eqtrd 2777 | . . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → (dom ◡{〈𝐴, 𝐵〉} ∩ dom ◡{〈𝐶, 𝐷〉}) = ∅) | 
| 15 |  | funun 6612 | . . 3
⊢ (((Fun
◡{〈𝐴, 𝐵〉} ∧ Fun ◡{〈𝐶, 𝐷〉}) ∧ (dom ◡{〈𝐴, 𝐵〉} ∩ dom ◡{〈𝐶, 𝐷〉}) = ∅) → Fun (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐶, 𝐷〉})) | 
| 16 | 3, 14, 15 | sylancr 587 | . 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐶, 𝐷〉})) | 
| 17 |  | df-pr 4629 | . . . . 5
⊢
{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ({〈𝐴, 𝐵〉} ∪ {〈𝐶, 𝐷〉}) | 
| 18 | 17 | cnveqi 5885 | . . . 4
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = ◡({〈𝐴, 𝐵〉} ∪ {〈𝐶, 𝐷〉}) | 
| 19 |  | cnvun 6162 | . . . 4
⊢ ◡({〈𝐴, 𝐵〉} ∪ {〈𝐶, 𝐷〉}) = (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐶, 𝐷〉}) | 
| 20 | 18, 19 | eqtri 2765 | . . 3
⊢ ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐶, 𝐷〉}) | 
| 21 | 20 | funeqi 6587 | . 2
⊢ (Fun
◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ↔ Fun (◡{〈𝐴, 𝐵〉} ∪ ◡{〈𝐶, 𝐷〉})) | 
| 22 | 16, 21 | sylibr 234 | 1
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |