Proof of Theorem elpglem2
| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . . 5
⊢
(1st ‘𝐴) ∈ V |
| 2 | | fvex 6919 |
. . . . 5
⊢
(2nd ‘𝐴) ∈ V |
| 3 | 1, 2 | unex 7764 |
. . . 4
⊢
((1st ‘𝐴) ∪ (2nd ‘𝐴)) ∈ V |
| 4 | 3 | isseti 3498 |
. . 3
⊢
∃𝑥 𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) |
| 5 | | sseq1 4009 |
. . . . . 6
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) → (𝑥 ⊆ Pg ↔
((1st ‘𝐴)
∪ (2nd ‘𝐴)) ⊆ Pg)) |
| 6 | | unss 4190 |
. . . . . 6
⊢
(((1st ‘𝐴) ⊆ Pg ∧ (2nd
‘𝐴) ⊆ Pg)
↔ ((1st ‘𝐴) ∪ (2nd ‘𝐴)) ⊆ Pg) |
| 7 | 5, 6 | bitr4di 289 |
. . . . 5
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) → (𝑥 ⊆ Pg ↔
((1st ‘𝐴)
⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg))) |
| 8 | 7 | biimprd 248 |
. . . 4
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(((1st ‘𝐴)
⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg) → 𝑥 ⊆ Pg)) |
| 9 | | ssun1 4178 |
. . . . . . 7
⊢
(1st ‘𝐴) ⊆ ((1st ‘𝐴) ∪ (2nd
‘𝐴)) |
| 10 | | id 22 |
. . . . . . 7
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) → 𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴))) |
| 11 | 9, 10 | sseqtrrid 4027 |
. . . . . 6
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(1st ‘𝐴)
⊆ 𝑥) |
| 12 | | vex 3484 |
. . . . . . 7
⊢ 𝑥 ∈ V |
| 13 | 12 | elpw2 5334 |
. . . . . 6
⊢
((1st ‘𝐴) ∈ 𝒫 𝑥 ↔ (1st ‘𝐴) ⊆ 𝑥) |
| 14 | 11, 13 | sylibr 234 |
. . . . 5
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(1st ‘𝐴)
∈ 𝒫 𝑥) |
| 15 | | ssun2 4179 |
. . . . . . 7
⊢
(2nd ‘𝐴) ⊆ ((1st ‘𝐴) ∪ (2nd
‘𝐴)) |
| 16 | 15, 10 | sseqtrrid 4027 |
. . . . . 6
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(2nd ‘𝐴)
⊆ 𝑥) |
| 17 | 12 | elpw2 5334 |
. . . . . 6
⊢
((2nd ‘𝐴) ∈ 𝒫 𝑥 ↔ (2nd ‘𝐴) ⊆ 𝑥) |
| 18 | 16, 17 | sylibr 234 |
. . . . 5
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(2nd ‘𝐴)
∈ 𝒫 𝑥) |
| 19 | 14, 18 | jca 511 |
. . . 4
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
((1st ‘𝐴)
∈ 𝒫 𝑥 ∧
(2nd ‘𝐴)
∈ 𝒫 𝑥)) |
| 20 | 8, 19 | jctird 526 |
. . 3
⊢ (𝑥 = ((1st ‘𝐴) ∪ (2nd
‘𝐴)) →
(((1st ‘𝐴)
⊆ Pg ∧ (2nd ‘𝐴) ⊆ Pg) → (𝑥 ⊆ Pg ∧ ((1st
‘𝐴) ∈ 𝒫
𝑥 ∧ (2nd
‘𝐴) ∈ 𝒫
𝑥)))) |
| 21 | 4, 20 | eximii 1837 |
. 2
⊢
∃𝑥(((1st ‘𝐴) ⊆ Pg ∧ (2nd
‘𝐴) ⊆ Pg)
→ (𝑥 ⊆ Pg ∧
((1st ‘𝐴)
∈ 𝒫 𝑥 ∧
(2nd ‘𝐴)
∈ 𝒫 𝑥))) |
| 22 | 21 | 19.37iv 1948 |
1
⊢
(((1st ‘𝐴) ⊆ Pg ∧ (2nd
‘𝐴) ⊆ Pg)
→ ∃𝑥(𝑥 ⊆ Pg ∧
((1st ‘𝐴)
∈ 𝒫 𝑥 ∧
(2nd ‘𝐴)
∈ 𝒫 𝑥))) |