Proof of Theorem funcnvqpOLD
Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → 𝐴 ∈ 𝑈) |
2 | 1 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) → 𝐴 ∈ 𝑈) |
3 | | simpr 477 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → 𝐶 ∈ 𝑉) |
4 | 3 | adantr 481 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) → 𝐶 ∈ 𝑉) |
5 | | simp11 1091 |
. . . 4
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻) → 𝐵 ≠ 𝐷) |
6 | | funcnvpr 5950 |
. . . 4
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
7 | 2, 4, 5, 6 | syl2an3an 1386 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉}) |
8 | | simpl 473 |
. . . . 5
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → 𝐸 ∈ 𝑊) |
9 | 8 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) → 𝐸 ∈ 𝑊) |
10 | | simpr 477 |
. . . . 5
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → 𝐺 ∈ 𝑇) |
11 | 10 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) → 𝐺 ∈ 𝑇) |
12 | | simp3 1063 |
. . . 4
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻) → 𝐹 ≠ 𝐻) |
13 | | funcnvpr 5950 |
. . . 4
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇 ∧ 𝐹 ≠ 𝐻) → Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
14 | 9, 11, 12, 13 | syl2an3an 1386 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
15 | | df-rn 5125 |
. . . . . 6
⊢ ran
{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} |
16 | | rnpropg 5615 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → ran {〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐵, 𝐷}) |
17 | 15, 16 | syl5eqr 2670 |
. . . . 5
⊢ ((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) → dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} = {𝐵, 𝐷}) |
18 | | df-rn 5125 |
. . . . . 6
⊢ ran
{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} = dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} |
19 | | rnpropg 5615 |
. . . . . 6
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → ran {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} = {𝐹, 𝐻}) |
20 | 18, 19 | syl5eqr 2670 |
. . . . 5
⊢ ((𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇) → dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉} = {𝐹, 𝐻}) |
21 | 17, 20 | ineqan12d 3816 |
. . . 4
⊢ (((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) → (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = ({𝐵, 𝐷} ∩ {𝐹, 𝐻})) |
22 | | simp2 1062 |
. . . . . . 7
⊢ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) → 𝐵 ≠ 𝐹) |
23 | | simpl 473 |
. . . . . . 7
⊢ ((𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) → 𝐷 ≠ 𝐹) |
24 | 22, 23 | anim12i 590 |
. . . . . 6
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻)) → (𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) |
25 | 24 | 3adant3 1081 |
. . . . 5
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻) → (𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹)) |
26 | | simp3 1063 |
. . . . . . 7
⊢ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) → 𝐵 ≠ 𝐻) |
27 | | simpr 477 |
. . . . . . 7
⊢ ((𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) → 𝐷 ≠ 𝐻) |
28 | 26, 27 | anim12i 590 |
. . . . . 6
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻)) → (𝐵 ≠ 𝐻 ∧ 𝐷 ≠ 𝐻)) |
29 | 28 | 3adant3 1081 |
. . . . 5
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻) → (𝐵 ≠ 𝐻 ∧ 𝐷 ≠ 𝐻)) |
30 | | disjpr2 4248 |
. . . . 5
⊢ (((𝐵 ≠ 𝐹 ∧ 𝐷 ≠ 𝐹) ∧ (𝐵 ≠ 𝐻 ∧ 𝐷 ≠ 𝐻)) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
31 | 25, 29, 30 | syl2anc 693 |
. . . 4
⊢ (((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻) → ({𝐵, 𝐷} ∩ {𝐹, 𝐻}) = ∅) |
32 | 21, 31 | sylan9eq 2676 |
. . 3
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = ∅) |
33 | | funun 5932 |
. . 3
⊢ (((Fun
◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∧ Fun ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) ∧ (dom ◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∩ dom ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = ∅) → Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |
34 | 7, 14, 32, 33 | syl21anc 1325 |
. 2
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |
35 | | cnvun 5538 |
. . 3
⊢ ◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) = (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) |
36 | 35 | funeqi 5909 |
. 2
⊢ (Fun
◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉}) ↔ Fun (◡{〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ ◡{〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |
37 | 34, 36 | sylibr 224 |
1
⊢ ((((𝐴 ∈ 𝑈 ∧ 𝐶 ∈ 𝑉) ∧ (𝐸 ∈ 𝑊 ∧ 𝐺 ∈ 𝑇)) ∧ ((𝐵 ≠ 𝐷 ∧ 𝐵 ≠ 𝐹 ∧ 𝐵 ≠ 𝐻) ∧ (𝐷 ≠ 𝐹 ∧ 𝐷 ≠ 𝐻) ∧ 𝐹 ≠ 𝐻)) → Fun ◡({〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉} ∪ {〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉})) |