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 R1 : On 1-1 V
2 omsson ω On
3 f1ores R1 : On 1-1 V ω On R1 ω : ω 1-1 onto R1 ω
4 1 2 3 mp2an R1 ω : ω 1-1 onto R1 ω
5 f1of1 R1 ω : ω 1-1 onto R1 ω R1 ω : ω 1-1 R1 ω
6 4 5 ax-mp R1 ω : ω 1-1 R1 ω
7 r1fnon R1 Fn On
8 fvelimab R1 Fn On ω On w R1 ω x ω R1 x = w
9 7 2 8 mp2an w R1 ω x ω R1 x = w
10 fveq2 x = R1 x = R1
11 10 eleq1d x = R1 x y R1 y
12 fveq2 x = w R1 x = R1 w
13 12 eleq1d x = w R1 x y R1 w y
14 fveq2 x = suc w R1 x = R1 suc w
15 14 eleq1d x = suc w R1 x y R1 suc w y
16 r10 R1 =
17 16 eleq1i R1 y y
18 17 biimpri y R1 y
19 18 adantr y z y 𝒫 z y R1 y
20 pweq z = R1 w 𝒫 z = 𝒫 R1 w
21 20 eleq1d z = R1 w 𝒫 z y 𝒫 R1 w y
22 21 rspccv z y 𝒫 z y R1 w y 𝒫 R1 w y
23 nnon w ω w On
24 r1suc w On R1 suc w = 𝒫 R1 w
25 23 24 syl w ω R1 suc w = 𝒫 R1 w
26 25 eleq1d w ω R1 suc w y 𝒫 R1 w y
27 26 biimprcd 𝒫 R1 w y w ω R1 suc w y
28 22 27 syl6 z y 𝒫 z y R1 w y w ω R1 suc w y
29 28 com3r w ω z y 𝒫 z y R1 w y R1 suc w y
30 29 adantld w ω y z y 𝒫 z y R1 w y R1 suc w y
31 11 13 15 19 30 finds2 x ω y z y 𝒫 z y R1 x y
32 eleq1 R1 x = w R1 x y w y
33 32 biimpd R1 x = w R1 x y w y
34 31 33 syl9 x ω R1 x = w y z y 𝒫 z y w y
35 34 rexlimiv x ω R1 x = w y z y 𝒫 z y w y
36 9 35 sylbi w R1 ω y z y 𝒫 z y w y
37 36 com12 y z y 𝒫 z y w R1 ω w y
38 37 ssrdv y z y 𝒫 z y R1 ω y
39 vex y V
40 39 ssex R1 ω y R1 ω V
41 38 40 syl y z y 𝒫 z y R1 ω V
42 0ex V
43 eleq1 x = x y y
44 43 anbi1d x = x y z y 𝒫 z y y z y 𝒫 z y
45 44 exbidv x = y x y z y 𝒫 z y y y z y 𝒫 z y
46 axgroth6 y x y z y 𝒫 z y 𝒫 z y z 𝒫 y z y z y
47 simpr 𝒫 z y 𝒫 z y 𝒫 z y
48 47 ralimi z y 𝒫 z y 𝒫 z y z y 𝒫 z y
49 48 anim2i x y z y 𝒫 z y 𝒫 z y x y z y 𝒫 z y
50 49 3adant3 x y z y 𝒫 z y 𝒫 z y z 𝒫 y z y z y x y z y 𝒫 z y
51 46 50 eximii y x y z y 𝒫 z y
52 42 45 51 vtocl y y z y 𝒫 z y
53 41 52 exlimiiv R1 ω V
54 f1dmex R1 ω : ω 1-1 R1 ω R1 ω V ω V
55 6 53 54 mp2an ω V