Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = ∅ → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∅ ) )
2 1 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑇 ↔ ( 𝑅1 ‘ ∅ ) ∈ 𝑇 ) )
3 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ 𝑦 ) )
4 3 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑇 ↔ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑇 ) )
5 fveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ suc 𝑦 ) )
6 5 eleq1d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑇 ↔ ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑇 ) )
7 r10 ⊢ ( 𝑅1 ‘ ∅ ) = ∅
8 tsk0 ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ∅ ∈ 𝑇 )
9 7 8 eqeltrid ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 ‘ ∅ ) ∈ 𝑇 )
10 tskpw ⊢ ( ( 𝑇 ∈ Tarski ∧ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑇 ) → 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑇 )
11 nnon ⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
12 r1suc ⊢ ( 𝑦 ∈ On → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
13 11 12 syl ⊢ ( 𝑦 ∈ ω → ( 𝑅1 ‘ suc 𝑦 ) = 𝒫 ( 𝑅1 ‘ 𝑦 ) )
14 13 eleq1d ⊢ ( 𝑦 ∈ ω → ( ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑇 ↔ 𝒫 ( 𝑅1 ‘ 𝑦 ) ∈ 𝑇 ) )
15 10 14 imbitrrid ⊢ ( 𝑦 ∈ ω → ( ( 𝑇 ∈ Tarski ∧ ( 𝑅1 ‘ 𝑦 ) ∈ 𝑇 ) → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑇 ) )
16 15 expd ⊢ ( 𝑦 ∈ ω → ( 𝑇 ∈ Tarski → ( ( 𝑅1 ‘ 𝑦 ) ∈ 𝑇 → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑇 ) ) )
17 16 adantrd ⊢ ( 𝑦 ∈ ω → ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( ( 𝑅1 ‘ 𝑦 ) ∈ 𝑇 → ( 𝑅1 ‘ suc 𝑦 ) ∈ 𝑇 ) ) )
18 2 4 6 9 17 finds2 ⊢ ( 𝑥 ∈ ω → ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑇 ) )
19 eleq1 ⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( ( 𝑅1 ‘ 𝑥 ) ∈ 𝑇 ↔ 𝑦 ∈ 𝑇 ) )
20 19 imbi2d ⊢ ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 ‘ 𝑥 ) ∈ 𝑇 ) ↔ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 𝑦 ∈ 𝑇 ) ) )
21 18 20 syl5ibcom ⊢ ( 𝑥 ∈ ω → ( ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 𝑦 ∈ 𝑇 ) ) )
22 21 rexlimiv ⊢ ( ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑦 → ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → 𝑦 ∈ 𝑇 ) )
23 r1fnon ⊢ 𝑅1 Fn On
24 fnfun ⊢ ( 𝑅1 Fn On → Fun 𝑅1 )
25 23 24 ax-mp ⊢ Fun 𝑅1
26 fvelima ⊢ ( ( Fun 𝑅1 ∧ 𝑦 ∈ ( 𝑅1 “ ω ) ) → ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
27 25 26 mpan ⊢ ( 𝑦 ∈ ( 𝑅1 “ ω ) → ∃ 𝑥 ∈ ω ( 𝑅1 ‘ 𝑥 ) = 𝑦 )
28 22 27 syl11 ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑦 ∈ ( 𝑅1 “ ω ) → 𝑦 ∈ 𝑇 ) )
29 28 ssrdv ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑇 ≠ ∅ ) → ( 𝑅1 “ ω ) ⊆ 𝑇 )