Proof of Theorem elpglem2
Step | Hyp | Ref
| Expression |
1 | | fvex 6730 |
. . . . 5
⊢
(1st ‘𝐴) ∈ V |
2 | | fvex 6730 |
. . . . 5
⊢
(2nd ‘𝐴) ∈ V |
3 | 1, 2 | unex 7531 |
. . . 4
⊢
((1st ‘𝐴) ∪ (2nd ‘𝐴)) ∈ V |
4 | 3 | isseti 3423 |
. . 3
⊢
∃𝑥 𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) |
5 | | sseq1 3926 |
. . . . . 6
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) → (𝑥 ⊆ Pg ↔
((1st ‘𝐴)
∪ (2nd ‘𝐴)) ⊆ Pg)) |
6 | | unss 4098 |
. . . . . 6
⊢
(((1st ‘𝐴) ⊆ Pg ∧ (2nd
‘𝐴) ⊆ Pg)
↔ ((1st ‘𝐴) ∪ (2nd ‘𝐴)) ⊆ Pg) |
7 | 5, 6 | bitr4di 292 |
. . . . 5
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) → (𝑥 ⊆ Pg ↔
((1st ‘𝐴)
⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg))) |
8 | 7 | biimprd 251 |
. . . 4
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(((1st ‘𝐴)
⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg) → 𝑥 ⊆ Pg)) |
9 | | ssun1 4086 |
. . . . . . 7
⊢
(1st ‘𝐴) ⊆ ((1st ‘𝐴) ∪ (2nd
‘𝐴)) |
10 | | id 22 |
. . . . . . 7
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) → 𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴))) |
11 | 9, 10 | sseqtrrid 3954 |
. . . . . 6
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(1st ‘𝐴)
⊆ 𝑥) |
12 | | vex 3412 |
. . . . . . 7
⊢ 𝑥 ∈ V |
13 | 12 | elpw2 5238 |
. . . . . 6
⊢
((1st ‘𝐴) ∈ 𝒫 𝑥 ↔ (1st ‘𝐴) ⊆ 𝑥) |
14 | 11, 13 | sylibr 237 |
. . . . 5
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(1st ‘𝐴)
∈ 𝒫 𝑥) |
15 | | ssun2 4087 |
. . . . . . 7
⊢
(2nd ‘𝐴) ⊆ ((1st ‘𝐴) ∪ (2nd
‘𝐴)) |
16 | 15, 10 | sseqtrrid 3954 |
. . . . . 6
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(2nd ‘𝐴)
⊆ 𝑥) |
17 | 12 | elpw2 5238 |
. . . . . 6
⊢
((2nd ‘𝐴) ∈ 𝒫 𝑥 ↔ (2nd ‘𝐴) ⊆ 𝑥) |
18 | 16, 17 | sylibr 237 |
. . . . 5
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(2nd ‘𝐴)
∈ 𝒫 𝑥) |
19 | 14, 18 | jca 515 |
. . . 4
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
((1st ‘𝐴)
∈ 𝒫 𝑥 ∧
(2nd ‘𝐴)
∈ 𝒫 𝑥)) |
20 | 8, 19 | jctird 530 |
. . 3
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(((1st ‘𝐴)
⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg) → (𝑥 ⊆ Pg ∧ ((1st
‘𝐴) ∈ 𝒫
𝑥 ∧ (2nd
‘𝐴) ∈ 𝒫
𝑥)))) |
21 | 4, 20 | eximii 1844 |
. 2
⊢
∃𝑥(((1st ‘𝐴) ⊆ Pg ∧ (2nd
‘𝐴) ⊆ Pg)
→ (𝑥 ⊆ Pg ∧
((1st ‘𝐴)
∈ 𝒫 𝑥 ∧
(2nd ‘𝐴)
∈ 𝒫 𝑥))) |
22 | 21 | 19.37iv 1957 |
1
⊢
(((1st ‘𝐴) ⊆ Pg ∧ (2nd
‘𝐴) ⊆ Pg)
→ ∃𝑥(𝑥 ⊆ Pg ∧
((1st ‘𝐴)
∈ 𝒫 𝑥 ∧
(2nd ‘𝐴)
∈ 𝒫 𝑥))) |