Step | Hyp | Ref
| Expression |
1 | | simprr 531 |
. . . 4
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → 𝐶 = ∪ ◡{𝐵}) |
2 | | 1st2nd 6182 |
. . . . . . . 8
⊢ ((Rel
𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 = ⟨(1st ‘𝐵), (2nd ‘𝐵)⟩) |
3 | 2 | adantrr 479 |
. . . . . . 7
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → 𝐵 = ⟨(1st ‘𝐵), (2nd ‘𝐵)⟩) |
4 | 3 | sneqd 3606 |
. . . . . 6
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → {𝐵} = {⟨(1st ‘𝐵), (2nd ‘𝐵)⟩}) |
5 | 4 | cnveqd 4804 |
. . . . 5
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ◡{𝐵} = ◡{⟨(1st ‘𝐵), (2nd ‘𝐵)⟩}) |
6 | 5 | unieqd 3821 |
. . . 4
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ∪
◡{𝐵} = ∪ ◡{⟨(1st ‘𝐵), (2nd ‘𝐵)⟩}) |
7 | | 1stexg 6168 |
. . . . . 6
⊢ (𝐵 ∈ 𝐴 → (1st ‘𝐵) ∈ V) |
8 | | 2ndexg 6169 |
. . . . . 6
⊢ (𝐵 ∈ 𝐴 → (2nd ‘𝐵) ∈ V) |
9 | | opswapg 5116 |
. . . . . 6
⊢
(((1st ‘𝐵) ∈ V ∧ (2nd
‘𝐵) ∈ V) →
∪ ◡{⟨(1st ‘𝐵), (2nd ‘𝐵)⟩} = ⟨(2nd
‘𝐵), (1st
‘𝐵)⟩) |
10 | 7, 8, 9 | syl2anc 411 |
. . . . 5
⊢ (𝐵 ∈ 𝐴 → ∪ ◡{⟨(1st ‘𝐵), (2nd ‘𝐵)⟩} = ⟨(2nd
‘𝐵), (1st
‘𝐵)⟩) |
11 | 10 | ad2antrl 490 |
. . . 4
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ∪
◡{⟨(1st ‘𝐵), (2nd ‘𝐵)⟩} = ⟨(2nd
‘𝐵), (1st
‘𝐵)⟩) |
12 | 1, 6, 11 | 3eqtrd 2214 |
. . 3
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → 𝐶 = ⟨(2nd ‘𝐵), (1st ‘𝐵)⟩) |
13 | | simprl 529 |
. . . . 5
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → 𝐵 ∈ 𝐴) |
14 | 3, 13 | eqeltrrd 2255 |
. . . 4
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ⟨(1st
‘𝐵), (2nd
‘𝐵)⟩ ∈
𝐴) |
15 | | opelcnvg 4808 |
. . . . . 6
⊢
(((2nd ‘𝐵) ∈ V ∧ (1st
‘𝐵) ∈ V) →
(⟨(2nd ‘𝐵), (1st ‘𝐵)⟩ ∈ ◡𝐴 ↔ ⟨(1st ‘𝐵), (2nd ‘𝐵)⟩ ∈ 𝐴)) |
16 | 8, 7, 15 | syl2anc 411 |
. . . . 5
⊢ (𝐵 ∈ 𝐴 → (⟨(2nd ‘𝐵), (1st ‘𝐵)⟩ ∈ ◡𝐴 ↔ ⟨(1st ‘𝐵), (2nd ‘𝐵)⟩ ∈ 𝐴)) |
17 | 16 | ad2antrl 490 |
. . . 4
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → (⟨(2nd
‘𝐵), (1st
‘𝐵)⟩ ∈
◡𝐴 ↔ ⟨(1st ‘𝐵), (2nd ‘𝐵)⟩ ∈ 𝐴)) |
18 | 14, 17 | mpbird 167 |
. . 3
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ⟨(2nd
‘𝐵), (1st
‘𝐵)⟩ ∈
◡𝐴) |
19 | 12, 18 | eqeltrd 2254 |
. 2
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → 𝐶 ∈ ◡𝐴) |
20 | | opswapg 5116 |
. . . . . 6
⊢
(((2nd ‘𝐵) ∈ V ∧ (1st
‘𝐵) ∈ V) →
∪ ◡{⟨(2nd ‘𝐵), (1st ‘𝐵)⟩} = ⟨(1st
‘𝐵), (2nd
‘𝐵)⟩) |
21 | 8, 7, 20 | syl2anc 411 |
. . . . 5
⊢ (𝐵 ∈ 𝐴 → ∪ ◡{⟨(2nd ‘𝐵), (1st ‘𝐵)⟩} = ⟨(1st
‘𝐵), (2nd
‘𝐵)⟩) |
22 | 21 | eqcomd 2183 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → ⟨(1st ‘𝐵), (2nd ‘𝐵)⟩ = ∪ ◡{⟨(2nd ‘𝐵), (1st ‘𝐵)⟩}) |
23 | 22 | ad2antrl 490 |
. . 3
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ⟨(1st
‘𝐵), (2nd
‘𝐵)⟩ = ∪ ◡{⟨(2nd ‘𝐵), (1st ‘𝐵)⟩}) |
24 | 12 | sneqd 3606 |
. . . . 5
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → {𝐶} = {⟨(2nd ‘𝐵), (1st ‘𝐵)⟩}) |
25 | 24 | cnveqd 4804 |
. . . 4
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ◡{𝐶} = ◡{⟨(2nd ‘𝐵), (1st ‘𝐵)⟩}) |
26 | 25 | unieqd 3821 |
. . 3
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → ∪
◡{𝐶} = ∪ ◡{⟨(2nd ‘𝐵), (1st ‘𝐵)⟩}) |
27 | 23, 3, 26 | 3eqtr4d 2220 |
. 2
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → 𝐵 = ∪ ◡{𝐶}) |
28 | 19, 27 | jca 306 |
1
⊢ ((Rel
𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 = ∪ ◡{𝐵})) → (𝐶 ∈ ◡𝐴 ∧ 𝐵 = ∪ ◡{𝐶})) |