Proof of Theorem funcnvqp
Step | Hyp | Ref
| Expression |
1 | | funcnvpr 6606 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
2 | 1 | 3expa 1119 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ 𝐵 ≠ 𝐷) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
3 | 2 | 3ad2antr1 1189 |
. . . . 5
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻)) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
4 | 3 | ad2ant2r 746 |
. . . 4
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
5 | 4 | 3adantr2 1171 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
6 | | funcnvpr 6606 |
. . . . . 6
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ∧ 𝐹 ≠ 𝐻) → Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
7 | 6 | 3expa 1119 |
. . . . 5
⊢ (((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) ∧ 𝐹 ≠ 𝐻) → Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
8 | 7 | ad2ant2l 745 |
. . . 4
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
9 | 8 | 3adantr2 1171 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
10 | | df-rn 5685 |
. . . . . 6
⊢ ran
{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} |
11 | | rnpropg 6217 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → ran {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐵, 𝐷}) |
12 | 10, 11 | eqtr3id 2787 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐵, 𝐷}) |
13 | | df-rn 5685 |
. . . . . 6
⊢ ran
{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} = dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} |
14 | | rnpropg 6217 |
. . . . . 6
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → ran {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} = {𝐹, 𝐻}) |
15 | 13, 14 | eqtr3id 2787 |
. . . . 5
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} = {𝐹, 𝐻}) |
16 | 12, 15 | ineqan12d 4212 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) → (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = ({𝐵, 𝐷} ∩ {𝐹, 𝐻})) |
17 | | disjpr2 4715 |
. . . . . . 7
⊢ (((𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) ∧ (𝐵 ≠ 𝐻 ∧ 𝐷 ≠ 𝐻)) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
18 | 17 | an4s 659 |
. . . . . 6
⊢ (((𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻)) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
19 | 18 | 3adantl1 1167 |
. . . . 5
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻)) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
20 | 19 | 3adant3 1133 |
. . . 4
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
21 | 16, 20 | sylan9eq 2793 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = ∅) |
22 | | funun 6590 |
. . 3
⊢ (((Fun
◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∧ Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) ∧ (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = ∅) → Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |
23 | 5, 9, 21, 22 | syl21anc 837 |
. 2
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |
24 | | cnvun 6138 |
. . 3
⊢ ◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
25 | 24 | funeqi 6565 |
. 2
⊢ (Fun
◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) ↔ Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |
26 | 23, 25 | sylibr 233 |
1
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |