Theorem 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	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ∪ ( 𝑅1 “ ω ) ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		eluni2	⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ ω ) ↔ ∃ 𝑥 ∈ ( 𝑅1 “ ω ) 𝑦 ∈ 𝑥 )
2		r1fnon	⊢ 𝑅1 Fn On
3		fnfun	⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
4	2 3	ax-mp	⊢ Fun 𝑅1
5		fvelima	⊢ ( ( Fun 𝑅1 ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 )
6	4 5	mpan	⊢ ( 𝑥 ∈ ( 𝑅1 “ ω ) → ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 )
7		r1tr	⊢ Tr ( 𝑅1 ‘ 𝑦 )
8		treq	⊢ ( ( 𝑅1 ‘ 𝑦 ) = 𝑥 → ( Tr ( 𝑅1 ‘ 𝑦 ) ↔ Tr 𝑥 ) )
9	7 8	mpbii	⊢ ( ( 𝑅1 ‘ 𝑦 ) = 𝑥 → Tr 𝑥 )
10	9	rexlimivw	⊢ ( ∃ 𝑦 ∈ ω ( 𝑅1 ‘ 𝑦 ) = 𝑥 → Tr 𝑥 )
11		trss	⊢ ( Tr 𝑥 → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
12	6 10 11	3syl	⊢ ( 𝑥 ∈ ( 𝑅1 “ ω ) → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
13	12	adantl	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
14		tskr1om	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 “ ω ) ⊆ 𝑇 )
15	14	sseld	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑅1 “ ω ) → 𝑥 ∈ 𝑇 ) )
16		tskss	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ∈ 𝑇 ∧ 𝑦 ⊆ 𝑥 ) → 𝑦 ∈ 𝑇 )
17	16	3exp	⊢ ( 𝑇 ∈ Tarski → ( 𝑥 ∈ 𝑇 → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
18	17	adantr	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ 𝑇 → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
19	15 18	syld	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑥 ∈ ( 𝑅1 “ ω ) → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) ) )
20	19	imp	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ⊆ 𝑥 → 𝑦 ∈ 𝑇 ) )
21	13 20	syld	⊢ ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) ∧ 𝑥 ∈ ( 𝑅1 “ ω ) ) → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑇 ) )
22	21	rexlimdva	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( ∃ 𝑥 ∈ ( 𝑅1 “ ω ) 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑇 ) )
23	1 22	syl5bi	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑦 ∈ ∪ ( 𝑅1 “ ω ) → 𝑦 ∈ 𝑇 ) )
24	23	ssrdv	⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ∪ ( 𝑅1 “ ω ) ⊆ 𝑇 )