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 𝑦 ( 𝑥𝑦 ∧ ∀ 𝑧𝑦 ( 𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧𝑦𝑧𝑦 ) )

Proof

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