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