tskr1om2

Description: A nonempty Tarski class contains the whole finite cumulative hierarchy. (This proof does not use ax-inf .) (Contributed by NM, 22-Feb-2011)

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

Proof

Step	Hyp	Ref	Expression
1		eluni2	$⊢ y \in ⋃ R_{1} [ω] \leftrightarrow \exists x \in R_{1} [ω] y \in x$
2		r1fnon	$⊢ R_{1} Fn On$
3		fnfun	$⊢ R_{1} Fn On \to Fun R_{1}$
4	2 3	ax-mp	$⊢ Fun R_{1}$
5		fvelima	$⊢ (Fun R_{1} \land x \in R_{1} [ω]) \to \exists y \in ω R_{1} (y) = x$
6	4 5	mpan	$⊢ x \in R_{1} [ω] \to \exists y \in ω R_{1} (y) = x$
7		r1tr	$⊢ Tr R_{1} (y)$
8		treq	$⊢ R_{1} (y) = x \to (Tr R_{1} (y) \leftrightarrow Tr x)$
9	7 8	mpbii	$⊢ R_{1} (y) = x \to Tr x$
10	9	rexlimivw	$⊢ \exists y \in ω R_{1} (y) = x \to Tr x$
11		trss	$⊢ Tr x \to (y \in x \to y \subseteq x)$
12	6 10 11	3syl	$⊢ x \in R_{1} [ω] \to (y \in x \to y \subseteq x)$
13	12	adantl	$⊢ ((T \in Tarski \land T \neq \emptyset) \land x \in R_{1} [ω]) \to (y \in x \to y \subseteq x)$
14		tskr1om	$⊢ (T \in Tarski \land T \neq \emptyset) \to R_{1} [ω] \subseteq T$
15	14	sseld	$⊢ (T \in Tarski \land T \neq \emptyset) \to (x \in R_{1} [ω] \to x \in T)$
16		tskss	$⊢ (T \in Tarski \land x \in T \land y \subseteq x) \to y \in T$
17	16	3exp	$⊢ T \in Tarski \to (x \in T \to (y \subseteq x \to y \in T))$
18	17	adantr	$⊢ (T \in Tarski \land T \neq \emptyset) \to (x \in T \to (y \subseteq x \to y \in T))$
19	15 18	syld	$⊢ (T \in Tarski \land T \neq \emptyset) \to (x \in R_{1} [ω] \to (y \subseteq x \to y \in T))$
20	19	imp	$⊢ ((T \in Tarski \land T \neq \emptyset) \land x \in R_{1} [ω]) \to (y \subseteq x \to y \in T)$
21	13 20	syld	$⊢ ((T \in Tarski \land T \neq \emptyset) \land x \in R_{1} [ω]) \to (y \in x \to y \in T)$
22	21	rexlimdva	$⊢ (T \in Tarski \land T \neq \emptyset) \to (\exists x \in R_{1} [ω] y \in x \to y \in T)$
23	1 22	biimtrid	$⊢ (T \in Tarski \land T \neq \emptyset) \to (y \in ⋃ R_{1} [ω] \to y \in T)$
24	23	ssrdv	$⊢ (T \in Tarski \land T \neq \emptyset) \to ⋃ R_{1} [ω] \subseteq T$

Metamath Proof Explorer

Theorem tskr1om2

Proof