Metamath Proof Explorer


Theorem elpglem2

Description: Lemma for elpg . (Contributed by Emmett Weisz, 28-Aug-2021)

Ref Expression
Assertion elpglem2 1 st A Pg 2 nd A Pg x x Pg 1 st A 𝒫 x 2 nd A 𝒫 x

Proof

Step Hyp Ref Expression
1 fvex 1 st A V
2 fvex 2 nd A V
3 1 2 unex 1 st A 2 nd A V
4 3 isseti x x = 1 st A 2 nd A
5 sseq1 x = 1 st A 2 nd A x Pg 1 st A 2 nd A Pg
6 unss 1 st A Pg 2 nd A Pg 1 st A 2 nd A Pg
7 5 6 bitr4di x = 1 st A 2 nd A x Pg 1 st A Pg 2 nd A Pg
8 7 biimprd x = 1 st A 2 nd A 1 st A Pg 2 nd A Pg x Pg
9 ssun1 1 st A 1 st A 2 nd A
10 id x = 1 st A 2 nd A x = 1 st A 2 nd A
11 9 10 sseqtrrid x = 1 st A 2 nd A 1 st A x
12 vex x V
13 12 elpw2 1 st A 𝒫 x 1 st A x
14 11 13 sylibr x = 1 st A 2 nd A 1 st A 𝒫 x
15 ssun2 2 nd A 1 st A 2 nd A
16 15 10 sseqtrrid x = 1 st A 2 nd A 2 nd A x
17 12 elpw2 2 nd A 𝒫 x 2 nd A x
18 16 17 sylibr x = 1 st A 2 nd A 2 nd A 𝒫 x
19 14 18 jca x = 1 st A 2 nd A 1 st A 𝒫 x 2 nd A 𝒫 x
20 8 19 jctird x = 1 st A 2 nd A 1 st A Pg 2 nd A Pg x Pg 1 st A 𝒫 x 2 nd A 𝒫 x
21 4 20 eximii x 1 st A Pg 2 nd A Pg x Pg 1 st A 𝒫 x 2 nd A 𝒫 x
22 21 19.37iv 1 st A Pg 2 nd A Pg x x Pg 1 st A 𝒫 x 2 nd A 𝒫 x