This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grothomex

Description: The Tarski-Grothendieck Axiom implies the Axiom of Infinity (in the form of omex ). Note that our proof depends on neither the Axiom of Infinity nor Regularity. (Contributed by Mario Carneiro, 19-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion grothomex ω ∈ V

Proof

Step Hyp Ref Expression
1 r111 ⊢ 𝑅1 : On –1-1→ V
2 omsson ⊢ ω ⊆ On
3 f1ores ⊢ ( ( 𝑅1 : On –1-1→ V ∧ ω ⊆ On ) → ( 𝑅1 ↾ ω ) : ω –1-1-onto→ ( 𝑅1 “ ω ) )
4 1 2 3 mp2an ⊢ ( 𝑅1 ↾ ω ) : ω –1-1-onto→ ( 𝑅1 “ ω )
5 f1of1 ⊢ ( ( 𝑅1 ↾ ω ) : ω –1-1-onto→ ( 𝑅1 “ ω ) → ( 𝑅1 ↾ ω ) : ω –1-1→ ( 𝑅1 “ ω ) )
6 4 5 ax-mp ⊢ ( 𝑅1 ↾ ω ) : ω –1-1→ ( 𝑅1 “ ω )
7 r1fnon ⊢ 𝑅1 Fn On
8 fvelimab ⊢ ( ( 𝑅1 Fn On ∧ ω ⊆ On ) → ( 𝑤 ∈ ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑤 ) )
9 7 2 8 mp2an ⊢ ( 𝑤 ∈ ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑤 )
10 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
11 10 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 ↔ ( 𝑅1 ‘ ∅ ) ∈ 𝑦 ) )
12 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑤 ) )
13 12 eleq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 ↔ ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 ) )
14 fveq2 ⊢ ( 𝑥 = suc 𝑤 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑤 ) )
15 14 eleq1d ⊢ ( 𝑥 = suc 𝑤 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 ↔ ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) )
16 r10 ⊢ ( 𝑅1 ‘ ∅ ) = ∅
17 16 eleq1i ⊢ ( ( 𝑅1 ‘ ∅ ) ∈ 𝑦 ↔ ∅ ∈ 𝑦 )
18 17 biimpri ⊢ ( ∅ ∈ 𝑦 → ( 𝑅1 ‘ ∅ ) ∈ 𝑦 )
19 18 adantr ⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 ‘ ∅ ) ∈ 𝑦 )
20 pweq ⊢ ( 𝑧 = ( 𝑅1 ‘ 𝑤 ) → 𝒫 𝑧 = 𝒫 ( 𝑅1 ‘ 𝑤 ) )
21 20 eleq1d ⊢ ( 𝑧 = ( 𝑅1 ‘ 𝑤 ) → ( 𝒫 𝑧 ∈ 𝑦 ↔ 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 ) )
22 21 rspccv ⊢ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 ) )
23 nnon ⊢ ( 𝑤 ∈ ω → 𝑤 ∈ On )
24 r1suc ⊢ ( 𝑤 ∈ On → ( 𝑅1 ‘ suc 𝑤 ) = 𝒫 ( 𝑅1 ‘ 𝑤 ) )
25 23 24 syl ⊢ ( 𝑤 ∈ ω → ( 𝑅1 ‘ suc 𝑤 ) = 𝒫 ( 𝑅1 ‘ 𝑤 ) )
26 25 eleq1d ⊢ ( 𝑤 ∈ ω → ( ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ↔ 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 ) )
27 26 biimprcd ⊢ ( 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑤 ∈ ω → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) )
28 22 27 syl6 ⊢ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑤 ∈ ω → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) ) )
29 28 com3r ⊢ ( 𝑤 ∈ ω → ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) ) )
30 29 adantld ⊢ ( 𝑤 ∈ ω → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) ) )
31 11 13 15 19 30 finds2 ⊢ ( 𝑥 ∈ ω → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 ) )
32 eleq1 ⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) )
33 32 biimpd ⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 → 𝑤 ∈ 𝑦 ) )
34 31 33 syl9 ⊢ ( 𝑥 ∈ ω → ( ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → 𝑤 ∈ 𝑦 ) ) )
35 34 rexlimiv ⊢ ( ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → 𝑤 ∈ 𝑦 ) )
36 9 35 sylbi ⊢ ( 𝑤 ∈ ( 𝑅1 “ ω ) → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → 𝑤 ∈ 𝑦 ) )
37 36 com12 ⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑤 ∈ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝑦 ) )
38 37 ssrdv ⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 “ ω ) ⊆ 𝑦 )
39 vex ⊢ 𝑦 ∈ V
40 39 ssex ⊢ ( ( 𝑅1 “ ω ) ⊆ 𝑦 → ( 𝑅1 “ ω ) ∈ V )
41 38 40 syl ⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 “ ω ) ∈ V )
42 0ex ⊢ ∅ ∈ V
43 eleq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝑦 ↔ ∅ ∈ 𝑦 ) )
44 43 anbi1d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ↔ ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ) )
45 44 exbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ) )
46 axgroth6 ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) )
47 simpr ⊢ ( ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) → 𝒫 𝑧 ∈ 𝑦 )
48 47 ralimi ⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 )
49 48 anim2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) )
50 49 3adant3 ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) )
51 46 50 eximii ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 )
52 42 45 51 vtocl ⊢ ∃ 𝑦 ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 )
53 41 52 exlimiiv ⊢ ( 𝑅1 “ ω ) ∈ V
54 f1dmex ⊢ ( ( ( 𝑅1 ↾ ω ) : ω –1-1→ ( 𝑅1 “ ω ) ∧ ( 𝑅1 “ ω ) ∈ V ) → ω ∈ V )
55 6 53 54 mp2an ⊢ ω ∈ V