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) Use omex instead. (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	biranri	⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 ‘ ∅ ) ∈ 𝑦 )
19		pweq	⊢ ( 𝑧 = ( 𝑅1 ‘ 𝑤 ) → 𝒫 𝑧 = 𝒫 ( 𝑅1 ‘ 𝑤 ) )
20	19	eleq1d	⊢ ( 𝑧 = ( 𝑅1 ‘ 𝑤 ) → ( 𝒫 𝑧 ∈ 𝑦 ↔ 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 ) )
21	20	rspccv	⊢ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 ) )
22		nnon	⊢ ( 𝑤 ∈ ω → 𝑤 ∈ On )
23		r1suc	⊢ ( 𝑤 ∈ On → ( 𝑅1 ‘ suc 𝑤 ) = 𝒫 ( 𝑅1 ‘ 𝑤 ) )
24	22 23	syl	⊢ ( 𝑤 ∈ ω → ( 𝑅1 ‘ suc 𝑤 ) = 𝒫 ( 𝑅1 ‘ 𝑤 ) )
25	24	eleq1d	⊢ ( 𝑤 ∈ ω → ( ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ↔ 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 ) )
26	25	biimprcd	⊢ ( 𝒫 ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑤 ∈ ω → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) )
27	21 26	syl6	⊢ ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑤 ∈ ω → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) ) )
28	27	com3r	⊢ ( 𝑤 ∈ ω → ( ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) ) )
29	28	adantld	⊢ ( 𝑤 ∈ ω → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( ( 𝑅1 ‘ 𝑤 ) ∈ 𝑦 → ( 𝑅1 ‘ suc 𝑤 ) ∈ 𝑦 ) ) )
30	11 13 15 18 29	finds2	⊢ ( 𝑥 ∈ ω → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 ) )
31		eleq1	⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 ↔ 𝑤 ∈ 𝑦 ) )
32	31	biimpd	⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑦 → 𝑤 ∈ 𝑦 ) )
33	30 32	syl9	⊢ ( 𝑥 ∈ ω → ( ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → 𝑤 ∈ 𝑦 ) ) )
34	33	rexlimiv	⊢ ( ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑤 → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → 𝑤 ∈ 𝑦 ) )
35	9 34	sylbi	⊢ ( 𝑤 ∈ ( 𝑅1 “ ω ) → ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → 𝑤 ∈ 𝑦 ) )
36	35	com12	⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑤 ∈ ( 𝑅1 “ ω ) → 𝑤 ∈ 𝑦 ) )
37	36	ssrdv	⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 “ ω ) ⊆ 𝑦 )
38		vex	⊢ 𝑦 ∈ V
39	38	ssex	⊢ ( ( 𝑅1 “ ω ) ⊆ 𝑦 → ( 𝑅1 “ ω ) ∈ V )
40	37 39	syl	⊢ ( ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) → ( 𝑅1 “ ω ) ∈ V )
41		0ex	⊢ ∅ ∈ V
42		eleq1	⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝑦 ↔ ∅ ∈ 𝑦 ) )
43	42	anbi1d	⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ↔ ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ) )
44	43	exbidv	⊢ ( 𝑥 = ∅ → ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) ) )
45		axgroth6	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) )
46		simpr	⊢ ( ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) → 𝒫 𝑧 ∈ 𝑦 )
47	46	ralimi	⊢ ( ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) → ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 )
48	47	anim2i	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) )
49	48	3adant3	⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( 𝒫 𝑧 ⊆ 𝑦 ∧ 𝒫 𝑧 ∈ 𝑦 ) ∧ ∀ 𝑧 ∈ 𝒫 𝑦 ( 𝑧 ≺ 𝑦 → 𝑧 ∈ 𝑦 ) ) → ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 ) )
50	45 49	eximii	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 )
51	41 44 50	vtocl	⊢ ∃ 𝑦 ( ∅ ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 𝒫 𝑧 ∈ 𝑦 )
52	40 51	exlimiiv	⊢ ( 𝑅1 “ ω ) ∈ V
53		f1dmex	⊢ ( ( ( 𝑅1 ↾ ω ) : ω –1-1→ ( 𝑅1 “ ω ) ∧ ( 𝑅1 “ ω ) ∈ V ) → ω ∈ V )
54	6 52 53	mp2an	⊢ ω ∈ V