This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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