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 ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) )