Step | Hyp | Ref
| Expression |
1 | | funcnvsn 6552 |
. . . 4
⊢ Fun ◡{⟨𝐴, 𝐵⟩} |
2 | | funcnvsn 6552 |
. . . 4
⊢ Fun ◡{⟨𝐶, 𝐷⟩} |
3 | 1, 2 | pm3.2i 472 |
. . 3
⊢ (Fun
◡{⟨𝐴, 𝐵⟩} ∧ Fun ◡{⟨𝐶, 𝐷⟩}) |
4 | | df-rn 5645 |
. . . . . . 7
⊢ ran
{⟨𝐴, 𝐵⟩} = dom ◡{⟨𝐴, 𝐵⟩} |
5 | | rnsnopg 6174 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑈 → ran {⟨𝐴, 𝐵⟩} = {𝐵}) |
6 | 4, 5 | eqtr3id 2787 |
. . . . . 6
⊢ (𝐴 ∈ 𝑈 → dom ◡{⟨𝐴, 𝐵⟩} = {𝐵}) |
7 | | df-rn 5645 |
. . . . . . 7
⊢ ran
{⟨𝐶, 𝐷⟩} = dom ◡{⟨𝐶, 𝐷⟩} |
8 | | rnsnopg 6174 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑉 → ran {⟨𝐶, 𝐷⟩} = {𝐷}) |
9 | 7, 8 | eqtr3id 2787 |
. . . . . 6
⊢ (𝐶 ∈ 𝑉 → dom ◡{⟨𝐶, 𝐷⟩} = {𝐷}) |
10 | 6, 9 | ineqan12d 4175 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → (dom ◡{⟨𝐴, 𝐵⟩} ∩ dom ◡{⟨𝐶, 𝐷⟩}) = ({𝐵} ∩ {𝐷})) |
11 | 10 | 3adant3 1133 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → (dom ◡{⟨𝐴, 𝐵⟩} ∩ dom ◡{⟨𝐶, 𝐷⟩}) = ({𝐵} ∩ {𝐷})) |
12 | | disjsn2 4674 |
. . . . 5
⊢ (𝐵 ≠ 𝐷 → ({𝐵} ∩ {𝐷}) = ∅) |
13 | 12 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → ({𝐵} ∩ {𝐷}) = ∅) |
14 | 11, 13 | eqtrd 2773 |
. . 3
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → (dom ◡{⟨𝐴, 𝐵⟩} ∩ dom ◡{⟨𝐶, 𝐷⟩}) = ∅) |
15 | | funun 6548 |
. . 3
⊢ (((Fun
◡{⟨𝐴, 𝐵⟩} ∧ Fun ◡{⟨𝐶, 𝐷⟩}) ∧ (dom ◡{⟨𝐴, 𝐵⟩} ∩ dom ◡{⟨𝐶, 𝐷⟩}) = ∅) → Fun (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐶, 𝐷⟩})) |
16 | 3, 14, 15 | sylancr 588 |
. 2
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐶, 𝐷⟩})) |
17 | | df-pr 4590 |
. . . . 5
⊢
{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) |
18 | 17 | cnveqi 5831 |
. . . 4
⊢ ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ◡({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) |
19 | | cnvun 6096 |
. . . 4
⊢ ◡({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) = (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐶, 𝐷⟩}) |
20 | 18, 19 | eqtri 2761 |
. . 3
⊢ ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐶, 𝐷⟩}) |
21 | 20 | funeqi 6523 |
. 2
⊢ (Fun
◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ↔ Fun (◡{⟨𝐴, 𝐵⟩} ∪ ◡{⟨𝐶, 𝐷⟩})) |
22 | 16, 21 | sylibr 233 |
1
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}) |