Proof of Theorem elxp6
Step | Hyp | Ref
| Expression |
1 | | elex 2566 |
. 2
⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 ∈ V) |
2 | | opexg 3964 |
. . . 4
⊢
(((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶) → 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
V) |
3 | 2 | adantl 262 |
. . 3
⊢ ((𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 ∧
((1st ‘𝐴)
∈ 𝐵 ∧
(2nd ‘𝐴)
∈ 𝐶)) →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ V) |
4 | | eleq1 2100 |
. . . 4
⊢ (𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 →
(𝐴 ∈ V ↔
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ V)) |
5 | 4 | adantr 261 |
. . 3
⊢ ((𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 ∧
((1st ‘𝐴)
∈ 𝐵 ∧
(2nd ‘𝐴)
∈ 𝐶)) → (𝐴 ∈ V ↔
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ V)) |
6 | 3, 5 | mpbird 156 |
. 2
⊢ ((𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 ∧
((1st ‘𝐴)
∈ 𝐵 ∧
(2nd ‘𝐴)
∈ 𝐶)) → 𝐴 ∈ V) |
7 | | 1stvalg 5769 |
. . . . . 6
⊢ (𝐴 ∈ V → (1st
‘𝐴) = ∪ dom {𝐴}) |
8 | | 2ndvalg 5770 |
. . . . . 6
⊢ (𝐴 ∈ V → (2nd
‘𝐴) = ∪ ran {𝐴}) |
9 | 7, 8 | opeq12d 3557 |
. . . . 5
⊢ (𝐴 ∈ V →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 = 〈∪
dom {𝐴}, ∪ ran {𝐴}〉) |
10 | 9 | eqeq2d 2051 |
. . . 4
⊢ (𝐴 ∈ V → (𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 ↔
𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉)) |
11 | 7 | eleq1d 2106 |
. . . . 5
⊢ (𝐴 ∈ V →
((1st ‘𝐴)
∈ 𝐵 ↔ ∪ dom {𝐴} ∈ 𝐵)) |
12 | 8 | eleq1d 2106 |
. . . . 5
⊢ (𝐴 ∈ V →
((2nd ‘𝐴)
∈ 𝐶 ↔ ∪ ran {𝐴} ∈ 𝐶)) |
13 | 11, 12 | anbi12d 442 |
. . . 4
⊢ (𝐴 ∈ V →
(((1st ‘𝐴)
∈ 𝐵 ∧
(2nd ‘𝐴)
∈ 𝐶) ↔ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶))) |
14 | 10, 13 | anbi12d 442 |
. . 3
⊢ (𝐴 ∈ V → ((𝐴 = 〈(1st
‘𝐴), (2nd
‘𝐴)〉 ∧
((1st ‘𝐴)
∈ 𝐵 ∧
(2nd ‘𝐴)
∈ 𝐶)) ↔ (𝐴 = 〈∪ dom {𝐴}, ∪ ran {𝐴}〉 ∧ (∪ dom {𝐴} ∈ 𝐵 ∧ ∪ ran
{𝐴} ∈ 𝐶)))) |
15 | | elxp4 4808 |
. . 3
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈∪ dom
{𝐴}, ∪ ran {𝐴}〉 ∧ (∪
dom {𝐴} ∈ 𝐵 ∧ ∪ ran {𝐴} ∈ 𝐶))) |
16 | 14, 15 | syl6rbbr 188 |
. 2
⊢ (𝐴 ∈ V → (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st
‘𝐴) ∈ 𝐵 ∧ (2nd
‘𝐴) ∈ 𝐶)))) |
17 | 1, 6, 16 | pm5.21nii 620 |
1
⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st
‘𝐴) ∈ 𝐵 ∧ (2nd
‘𝐴) ∈ 𝐶))) |