Metamath Proof Explorer


Theorem axgroth6

Description: The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set x , there exists a set y containing x , the subsets of the members of y , the power sets of the members of y , and the subsets of y of cardinality less than that of y . (Contributed by NM, 21-Jun-2009)

Ref Expression
Assertion axgroth6 y x y z y 𝒫 z y 𝒫 z y z 𝒫 y z y z y

Proof

Step Hyp Ref Expression
1 axgroth5 y x y z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y
2 biid x y x y
3 pweq z = v 𝒫 z = 𝒫 v
4 3 sseq1d z = v 𝒫 z y 𝒫 v y
5 4 cbvralvw z y 𝒫 z y v y 𝒫 v y
6 ssid 𝒫 z 𝒫 z
7 sseq2 w = 𝒫 z 𝒫 z w 𝒫 z 𝒫 z
8 7 rspcev 𝒫 z y 𝒫 z 𝒫 z w y 𝒫 z w
9 6 8 mpan2 𝒫 z y w y 𝒫 z w
10 pweq v = w 𝒫 v = 𝒫 w
11 10 sseq1d v = w 𝒫 v y 𝒫 w y
12 11 rspccv v y 𝒫 v y w y 𝒫 w y
13 pwss 𝒫 w y v v w v y
14 vpwex 𝒫 z V
15 sseq1 v = 𝒫 z v w 𝒫 z w
16 eleq1 v = 𝒫 z v y 𝒫 z y
17 15 16 imbi12d v = 𝒫 z v w v y 𝒫 z w 𝒫 z y
18 14 17 spcv v v w v y 𝒫 z w 𝒫 z y
19 13 18 sylbi 𝒫 w y 𝒫 z w 𝒫 z y
20 12 19 syl6 v y 𝒫 v y w y 𝒫 z w 𝒫 z y
21 20 rexlimdv v y 𝒫 v y w y 𝒫 z w 𝒫 z y
22 9 21 impbid2 v y 𝒫 v y 𝒫 z y w y 𝒫 z w
23 22 ralbidv v y 𝒫 v y z y 𝒫 z y z y w y 𝒫 z w
24 5 23 sylbi z y 𝒫 z y z y 𝒫 z y z y w y 𝒫 z w
25 24 pm5.32i z y 𝒫 z y z y 𝒫 z y z y 𝒫 z y z y w y 𝒫 z w
26 r19.26 z y 𝒫 z y 𝒫 z y z y 𝒫 z y z y 𝒫 z y
27 r19.26 z y 𝒫 z y w y 𝒫 z w z y 𝒫 z y z y w y 𝒫 z w
28 25 26 27 3bitr4i z y 𝒫 z y 𝒫 z y z y 𝒫 z y w y 𝒫 z w
29 velpw z 𝒫 y z y
30 impexp z y z y ¬ z y z y z y z y ¬ z y z y
31 ssdomg y V z y z y
32 31 elv z y z y
33 32 pm4.71i z y z y z y
34 33 imbi1i z y ¬ z y z y z y z y ¬ z y z y
35 brsdom z y z y ¬ z y
36 35 imbi1i z y z y z y ¬ z y z y
37 impexp z y ¬ z y z y z y ¬ z y z y
38 36 37 bitri z y z y z y ¬ z y z y
39 38 imbi2i z y z y z y z y z y ¬ z y z y
40 30 34 39 3bitr4ri z y z y z y z y ¬ z y z y
41 40 pm5.74ri z y z y z y ¬ z y z y
42 pm4.64 ¬ z y z y z y z y
43 41 42 bitrdi z y z y z y z y z y
44 29 43 sylbi z 𝒫 y z y z y z y z y
45 44 ralbiia z 𝒫 y z y z y z 𝒫 y z y z y
46 2 28 45 3anbi123i x y z y 𝒫 z y 𝒫 z y z 𝒫 y z y z y x y z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y
47 46 exbii y x y z y 𝒫 z y 𝒫 z y z 𝒫 y z y z y y x y z y 𝒫 z y w y 𝒫 z w z 𝒫 y z y z y
48 1 47 mpbir y x y z y 𝒫 z y 𝒫 z y z 𝒫 y z y z y