Step | Hyp | Ref
| Expression |
1 | | coundir 6220 |
. . . 4
⊢
(({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) = (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩})) |
2 | | brprop.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
3 | | brprop.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
4 | | coprprop.e |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ 𝑋) |
5 | 2, 3, 4 | cosnop 31711 |
. . . . . 6
⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) = {⟨𝐸, 𝐵⟩}) |
6 | | brprop.d |
. . . . . . 7
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
7 | | mptprop.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≠ 𝐶) |
8 | 7 | necomd 2995 |
. . . . . . 7
⊢ (𝜑 → 𝐶 ≠ 𝐴) |
9 | 6, 4, 8 | cosnopne 31710 |
. . . . . 6
⊢ (𝜑 → ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩}) = ∅) |
10 | 5, 9 | uneq12d 4144 |
. . . . 5
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩})) = ({⟨𝐸, 𝐵⟩} ∪ ∅)) |
11 | | un0 4370 |
. . . . 5
⊢
({⟨𝐸, 𝐵⟩} ∪ ∅) =
{⟨𝐸, 𝐵⟩} |
12 | 10, 11 | eqtrdi 2787 |
. . . 4
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐸, 𝐴⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩})) = {⟨𝐸, 𝐵⟩}) |
13 | 1, 12 | eqtrid 2783 |
. . 3
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) = {⟨𝐸, 𝐵⟩}) |
14 | | coundir 6220 |
. . . 4
⊢
(({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩}) = (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩})) |
15 | | coprprop.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ 𝑋) |
16 | 3, 15, 7 | cosnopne 31710 |
. . . . . 6
⊢ (𝜑 → ({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) = ∅) |
17 | | brprop.c |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
18 | 17, 6, 15 | cosnop 31711 |
. . . . . 6
⊢ (𝜑 → ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩}) = {⟨𝐹, 𝐷⟩}) |
19 | 16, 18 | uneq12d 4144 |
. . . . 5
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩})) = (∅ ∪ {⟨𝐹, 𝐷⟩})) |
20 | | 0un 4372 |
. . . . 5
⊢ (∅
∪ {⟨𝐹, 𝐷⟩}) = {⟨𝐹, 𝐷⟩} |
21 | 19, 20 | eqtrdi 2787 |
. . . 4
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ∘ {⟨𝐹, 𝐶⟩}) ∪ ({⟨𝐶, 𝐷⟩} ∘ {⟨𝐹, 𝐶⟩})) = {⟨𝐹, 𝐷⟩}) |
22 | 14, 21 | eqtrid 2783 |
. . 3
⊢ (𝜑 → (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩}) = {⟨𝐹, 𝐷⟩}) |
23 | 13, 22 | uneq12d 4144 |
. 2
⊢ (𝜑 → ((({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) ∪ (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩})) = ({⟨𝐸, 𝐵⟩} ∪ {⟨𝐹, 𝐷⟩})) |
24 | | df-pr 4609 |
. . . 4
⊢
{⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} = ({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) |
25 | | df-pr 4609 |
. . . 4
⊢
{⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩} = ({⟨𝐸, 𝐴⟩} ∪ {⟨𝐹, 𝐶⟩}) |
26 | 24, 25 | coeq12i 5839 |
. . 3
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ ({⟨𝐸, 𝐴⟩} ∪ {⟨𝐹, 𝐶⟩})) |
27 | | coundi 6219 |
. . 3
⊢
(({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ ({⟨𝐸, 𝐴⟩} ∪ {⟨𝐹, 𝐶⟩})) = ((({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) ∪ (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩})) |
28 | 26, 27 | eqtri 2759 |
. 2
⊢
({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = ((({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐸, 𝐴⟩}) ∪ (({⟨𝐴, 𝐵⟩} ∪ {⟨𝐶, 𝐷⟩}) ∘ {⟨𝐹, 𝐶⟩})) |
29 | | df-pr 4609 |
. 2
⊢
{⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩} = ({⟨𝐸, 𝐵⟩} ∪ {⟨𝐹, 𝐷⟩}) |
30 | 23, 28, 29 | 3eqtr4g 2796 |
1
⊢ (𝜑 → ({⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩} ∘ {⟨𝐸, 𝐴⟩, ⟨𝐹, 𝐶⟩}) = {⟨𝐸, 𝐵⟩, ⟨𝐹, 𝐷⟩}) |