tskr1om

Description: A nonempty Tarski class is infinite, because it contains all the finite levels of the cumulative hierarchy. (This proof does not use ax-inf .) (Contributed by Mario Carneiro, 24-Jun-2013)

		Ref	Expression
	Assertion	tskr1om	$⊢ (T \in Tarski \land T \neq \emptyset) \to R_{1} [ω] \subseteq T$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ x = \emptyset \to R_{1} (x) = R_{1} (\emptyset)$
2	1	eleq1d	$⊢ x = \emptyset \to (R_{1} (x) \in T \leftrightarrow R_{1} (\emptyset) \in T)$
3		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
4	3	eleq1d	$⊢ x = y \to (R_{1} (x) \in T \leftrightarrow R_{1} (y) \in T)$
5		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
6	5	eleq1d	$⊢ x = suc y \to (R_{1} (x) \in T \leftrightarrow R_{1} (suc y) \in T)$
7		r10	$⊢ R_{1} (\emptyset) = \emptyset$
8		tsk0	$⊢ (T \in Tarski \land T \neq \emptyset) \to \emptyset \in T$
9	7 8	eqeltrid	$⊢ (T \in Tarski \land T \neq \emptyset) \to R_{1} (\emptyset) \in T$
10		tskpw	$⊢ (T \in Tarski \land R_{1} (y) \in T) \to 𝒫 R_{1} (y) \in T$
11		nnon	$⊢ y \in ω \to y \in On$
12		r1suc	$⊢ y \in On \to R_{1} (suc y) = 𝒫 R_{1} (y)$
13	11 12	syl	$⊢ y \in ω \to R_{1} (suc y) = 𝒫 R_{1} (y)$
14	13	eleq1d	$⊢ y \in ω \to (R_{1} (suc y) \in T \leftrightarrow 𝒫 R_{1} (y) \in T)$
15	10 14	syl5ibr	$⊢ y \in ω \to ((T \in Tarski \land R_{1} (y) \in T) \to R_{1} (suc y) \in T)$
16	15	expd	$⊢ y \in ω \to (T \in Tarski \to (R_{1} (y) \in T \to R_{1} (suc y) \in T))$
17	16	adantrd	$⊢ y \in ω \to ((T \in Tarski \land T \neq \emptyset) \to (R_{1} (y) \in T \to R_{1} (suc y) \in T))$
18	2 4 6 9 17	finds2	$⊢ x \in ω \to ((T \in Tarski \land T \neq \emptyset) \to R_{1} (x) \in T)$
19		eleq1	$⊢ R_{1} (x) = y \to (R_{1} (x) \in T \leftrightarrow y \in T)$
20	19	imbi2d	$⊢ R_{1} (x) = y \to (((T \in Tarski \land T \neq \emptyset) \to R_{1} (x) \in T) \leftrightarrow ((T \in Tarski \land T \neq \emptyset) \to y \in T))$
21	18 20	syl5ibcom	$⊢ x \in ω \to (R_{1} (x) = y \to ((T \in Tarski \land T \neq \emptyset) \to y \in T))$
22	21	rexlimiv	$⊢ \exists x \in ω R_{1} (x) = y \to ((T \in Tarski \land T \neq \emptyset) \to y \in T)$
23		r1fnon	$⊢ R_{1} Fn On$
24		fnfun	$⊢ R_{1} Fn On \to Fun R_{1}$
25	23 24	ax-mp	$⊢ Fun R_{1}$
26		fvelima	$⊢ (Fun R_{1} \land y \in R_{1} [ω]) \to \exists x \in ω R_{1} (x) = y$
27	25 26	mpan	$⊢ y \in R_{1} [ω] \to \exists x \in ω R_{1} (x) = y$
28	22 27	syl11	$⊢ (T \in Tarski \land T \neq \emptyset) \to (y \in R_{1} [ω] \to y \in T)$
29	28	ssrdv	$⊢ (T \in Tarski \land T \neq \emptyset) \to R_{1} [ω] \subseteq T$

Metamath Proof Explorer

Theorem tskr1om

Proof