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	biranri	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} (\emptyset) \in y$
19		pweq	$⊢ z = R_{1} (w) \to 𝒫 z = 𝒫 R_{1} (w)$
20	19	eleq1d	$⊢ z = R_{1} (w) \to (𝒫 z \in y \leftrightarrow 𝒫 R_{1} (w) \in y)$
21	20	rspccv	$⊢ \forall z \in y 𝒫 z \in y \to (R_{1} (w) \in y \to 𝒫 R_{1} (w) \in y)$
22		nnon	$⊢ w \in ω \to w \in On$
23		r1suc	$⊢ w \in On \to R_{1} (suc w) = 𝒫 R_{1} (w)$
24	22 23	syl	$⊢ w \in ω \to R_{1} (suc w) = 𝒫 R_{1} (w)$
25	24	eleq1d	$⊢ w \in ω \to (R_{1} (suc w) \in y \leftrightarrow 𝒫 R_{1} (w) \in y)$
26	25	biimprcd	$⊢ 𝒫 R_{1} (w) \in y \to (w \in ω \to R_{1} (suc w) \in y)$
27	21 26	syl6	$⊢ \forall z \in y 𝒫 z \in y \to (R_{1} (w) \in y \to (w \in ω \to R_{1} (suc w) \in y))$
28	27	com3r	$⊢ w \in ω \to (\forall z \in y 𝒫 z \in y \to (R_{1} (w) \in y \to R_{1} (suc w) \in y))$
29	28	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))$
30	11 13 15 18 29	finds2	$⊢ x \in ω \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} (x) \in y)$
31		eleq1	$⊢ R_{1} (x) = w \to (R_{1} (x) \in y \leftrightarrow w \in y)$
32	31	biimpd	$⊢ R_{1} (x) = w \to (R_{1} (x) \in y \to w \in y)$
33	30 32	syl9	$⊢ x \in ω \to (R_{1} (x) = w \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to w \in y))$
34	33	rexlimiv	$⊢ \exists x \in ω R_{1} (x) = w \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to w \in y)$
35	9 34	sylbi	$⊢ w \in R_{1} [ω] \to ((\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to w \in y)$
36	35	com12	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to (w \in R_{1} [ω] \to w \in y)$
37	36	ssrdv	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} [ω] \subseteq y$
38		vex	$⊢ y \in V$
39	38	ssex	$⊢ R_{1} [ω] \subseteq y \to R_{1} [ω] \in V$
40	37 39	syl	$⊢ (\emptyset \in y \land \forall z \in y 𝒫 z \in y) \to R_{1} [ω] \in V$
41		0ex	$⊢ \emptyset \in V$
42		eleq1	$⊢ x = \emptyset \to (x \in y \leftrightarrow \emptyset \in y)$
43	42	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))$
44	43	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))$
45		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))$
46		simpr	$⊢ (𝒫 z \subseteq y \land 𝒫 z \in y) \to 𝒫 z \in y$
47	46	ralimi	$⊢ \forall z \in y (𝒫 z \subseteq y \land 𝒫 z \in y) \to \forall z \in y 𝒫 z \in y$
48	47	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)$
49	48	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)$
50	45 49	eximii	$⊢ \exists y (x \in y \land \forall z \in y 𝒫 z \in y)$
51	41 44 50	vtocl	$⊢ \exists y (\emptyset \in y \land \forall z \in y 𝒫 z \in y)$
52	40 51	exlimiiv	$⊢ R_{1} [ω] \in V$
53		f1dmex	$⊢ (({R_{1} ↾}_{ω}) : ω \underset{1-1}{⟶} R_{1} [ω] \land R_{1} [ω] \in V) \to ω \in V$
54	6 52 53	mp2an	$⊢ ω \in V$

Metamath Proof Explorer

Theorem grothomex

Proof