Step | Hyp | Ref
| Expression |
1 | | funcnvpr 6609 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}) |
2 | 1 | 3expa 1116 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐷) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}) |
3 | 2 | 3ad2antr1 1186 |
. . . . 5
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻)) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}) |
4 | 3 | ad2ant2r 743 |
. . . 4
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}) |
5 | 4 | 3adantr2 1168 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩}) |
6 | | funcnvpr 6609 |
. . . . . 6
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ∧ 𝐹 ≠ 𝐻) → Fun ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) |
7 | 6 | 3expa 1116 |
. . . . 5
⊢ (((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 ≠ 𝐻) → Fun ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) |
8 | 7 | ad2ant2l 742 |
. . . 4
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) |
9 | 8 | 3adantr2 1168 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) |
10 | | df-rn 5686 |
. . . . . 6
⊢ ran
{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} |
11 | | rnpropg 6220 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → ran {⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐵, 𝐷}) |
12 | 10, 11 | eqtr3id 2784 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = {𝐵, 𝐷}) |
13 | | df-rn 5686 |
. . . . . 6
⊢ ran
{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩} = dom ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩} |
14 | | rnpropg 6220 |
. . . . . 6
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → ran {⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩} = {𝐹, 𝐻}) |
15 | 13, 14 | eqtr3id 2784 |
. . . . 5
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → dom ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩} = {𝐹, 𝐻}) |
16 | 12, 15 | ineqan12d 4213 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) → (dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∩ dom ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) = ({𝐵, 𝐷} ∩ {𝐹, 𝐻})) |
17 | | disjpr2 4716 |
. . . . . . 7
⊢ (((𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) ∧ (𝐵 ≠ 𝐻 ∧ 𝐷 ≠ 𝐻)) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
18 | 17 | an4s 656 |
. . . . . 6
⊢ (((𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻)) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
19 | 18 | 3adantl1 1164 |
. . . . 5
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻)) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
20 | 19 | 3adant3 1130 |
. . . 4
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
21 | 16, 20 | sylan9eq 2790 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → (dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∩ dom ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) = ∅) |
22 | | funun 6593 |
. . 3
⊢ (((Fun
◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∧ Fun ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) ∧ (dom ◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∩ dom ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) = ∅) → Fun (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩})) |
23 | 5, 9, 21, 22 | syl21anc 834 |
. 2
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩})) |
24 | | cnvun 6141 |
. . 3
⊢ ◡({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ {⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) = (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) |
25 | 24 | funeqi 6568 |
. 2
⊢ (Fun
◡({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ {⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩}) ↔ Fun (◡{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ ◡{⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩})) |
26 | 23, 25 | sylibr 233 |
1
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∪ {⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩})) |