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	$⊢ ω \in V$

Proof

Step	Hyp	Ref	Expression
1		r111	$⊢ R_{1} : On \underset{1-1}{⟶} V$
2		omsson	$⊢ ω \subseteq On$
3		f1ores	$⊢ (R_{1} : On \underset{1-1}{⟶} V \land ω \subseteq On) \to ({R_{1} ↾}_{ω}) : ω \underset{1-1 onto}{⟶} R_{1} [ω]$
4	1 2 3	mp2an	$⊢ ({R_{1} ↾}_{ω}) : ω \underset{1-1 onto}{⟶} R_{1} [ω]$
5		f1of1	$⊢ ({R_{1} ↾}_{ω}) : ω \underset{1-1 onto}{⟶} R_{1} [ω] \to ({R_{1} ↾}_{ω}) : ω \underset{1-1}{⟶} R_{1} [ω]$
6	4 5	ax-mp	$⊢ ({R_{1} ↾}_{ω}) : ω \underset{1-1}{⟶} R_{1} [ω]$
7		r1fnon	$⊢ R_{1} Fn On$
8		fvelimab	$⊢ (R_{1} Fn On \land ω \subseteq On) \to (w \in R_{1} [ω] \leftrightarrow \exists x \in ω R_{1} (x) = w)$
9	7 2 8	mp2an	$⊢ w \in R_{1} [ω] \leftrightarrow \exists x \in ω R_{1} (x) = w$
10		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
11	10	eleq1d	$⊢ x = \emptyset \to (R_{1} (x) \in y \leftrightarrow R_{1} (\emptyset) \in y)$
12		fveq2	$⊢ x = w \to R_{1} (x) = R_{1} (w)$
13	12	eleq1d	$⊢ x = w \to (R_{1} (x) \in y \leftrightarrow R_{1} (w) \in y)$
14		fveq2	$⊢ x = suc w \to R_{1} (x) = R_{1} (suc w)$
15	14	eleq1d	$⊢ x = suc w \to (R_{1} (x) \in y \leftrightarrow R_{1} (suc w) \in y)$
16		r10	$⊢ R_{1} (\emptyset) = \emptyset$
17	16	eleq1i	$⊢ R_{1} (\emptyset) \in y \leftrightarrow \emptyset \in y$
18	17	biimpri	$⊢ \emptyset \in y \to R_{1} (\emptyset) \in y$
19	18	adantr	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} (\emptyset) \in y$
20		pweq	$⊢ z = R_{1} (w) \to 𝒫 z = 𝒫 R_{1} (w)$
21	20	eleq1d	$⊢ z = R_{1} (w) \to (𝒫 z \in y \leftrightarrow 𝒫 R_{1} (w) \in y)$
22	21	rspccv	$⊢ \forall z \in y 𝒫 z \in y \to (R_{1} (w) \in y \to 𝒫 R_{1} (w) \in y)$
23		nnon	$⊢ w \in ω \to w \in On$
24		r1suc	$⊢ w \in On \to R_{1} (suc w) = 𝒫 R_{1} (w)$
25	23 24	syl	$⊢ w \in ω \to R_{1} (suc w) = 𝒫 R_{1} (w)$
26	25	eleq1d	$⊢ w \in ω \to (R_{1} (suc w) \in y \leftrightarrow 𝒫 R_{1} (w) \in y)$
27	26	biimprcd	$⊢ 𝒫 R_{1} (w) \in y \to (w \in ω \to R_{1} (suc w) \in y)$
28	22 27	syl6	$⊢ \forall z \in y 𝒫 z \in y \to (R_{1} (w) \in y \to (w \in ω \to R_{1} (suc w) \in y))$
29	28	com3r	$⊢ w \in ω \to (\forall z \in y 𝒫 z \in y \to (R_{1} (w) \in y \to R_{1} (suc w) \in y))$
30	29	adantld	$⊢ w \in ω \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to (R_{1} (w) \in y \to R_{1} (suc w) \in y))$
31	11 13 15 19 30	finds2	$⊢ x \in ω \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} (x) \in y)$
32		eleq1	$⊢ R_{1} (x) = w \to (R_{1} (x) \in y \leftrightarrow w \in y)$
33	32	biimpd	$⊢ R_{1} (x) = w \to (R_{1} (x) \in y \to w \in y)$
34	31 33	syl9	$⊢ x \in ω \to (R_{1} (x) = w \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to w \in y))$
35	34	rexlimiv	$⊢ \exists x \in ω R_{1} (x) = w \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to w \in y)$
36	9 35	sylbi	$⊢ w \in R_{1} [ω] \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to w \in y)$
37	36	com12	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to (w \in R_{1} [ω] \to w \in y)$
38	37	ssrdv	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} [ω] \subseteq y$
39		vex	$⊢ y \in V$
40	39	ssex	$⊢ R_{1} [ω] \subseteq y \to R_{1} [ω] \in V$
41	38 40	syl	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} [ω] \in V$
42		0ex	$⊢ \emptyset \in V$
43		eleq1	$⊢ x = \emptyset \to (x \in y \leftrightarrow \emptyset \in y)$
44	43	anbi1d	$⊢ x = \emptyset \to ((x \in y \land \forall z \in y 𝒫 z \in y) \leftrightarrow (\emptyset \in y \land \forall z \in y 𝒫 z \in y))$
45	44	exbidv	$⊢ x = \emptyset \to (\exists y (x \in y \land \forall z \in y 𝒫 z \in y) \leftrightarrow \exists y (\emptyset \in y \land \forall z \in y 𝒫 z \in y))$
46		axgroth6	$⊢ \exists y (x \in y \land \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \land \forall z \in 𝒫 y (z ≺ y \to z \in y))$
47		simpr	$⊢ (𝒫 z \subseteq y \land 𝒫 z \in y) \to 𝒫 z \in y$
48	47	ralimi	$⊢ \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \to \forall z \in y 𝒫 z \in y$
49	48	anim2i	$⊢ (x \in y \land \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y)) \to (x \in y \land \forall z \in y 𝒫 z \in y)$
50	49	3adant3	$⊢ (x \in y \land \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \land \forall z \in 𝒫 y (z ≺ y \to z \in y)) \to (x \in y \land \forall z \in y 𝒫 z \in y)$
51	46 50	eximii	$⊢ \exists y (x \in y \land \forall z \in y 𝒫 z \in y)$
52	42 45 51	vtocl	$⊢ \exists y (\emptyset \in y \land \forall z \in y 𝒫 z \in y)$
53	41 52	exlimiiv	$⊢ R_{1} [ω] \in V$
54		f1dmex	$⊢ (({R_{1} ↾}_{ω}) : ω \underset{1-1}{⟶} R_{1} [ω] \land R_{1} [ω] \in V) \to ω \in V$
55	6 53 54	mp2an	$⊢ ω \in V$

Metamath Proof Explorer

Theorem grothomex

Proof