Metamath Proof Explorer

Theorem tskord

Description: A Tarski class contains all ordinals smaller than it. (Contributed by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion tskord ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≺ 𝑇 ↔ 𝑦 ≺ 𝑇 ) )
2 1 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ↔ ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) ) )
3 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑇 ↔ 𝑦 ∈ 𝑇 ) )
4 2 3 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) → 𝑥 ∈ 𝑇 ) ↔ ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 ) ) )
5 breq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ≺ 𝑇 ↔ 𝐴 ≺ 𝑇 ) )
6 5 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ↔ ( 𝑇 ∈ Tarski ∧ 𝐴 ≺ 𝑇 ) ) )
7 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑇 ↔ 𝐴 ∈ 𝑇 ) )
8 6 7 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) → 𝑥 ∈ 𝑇 ) ↔ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 ) ) )
9 simplrl ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑇 ∈ Tarski )
10 onelss ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ 𝑥 ) )
11 ssdomg ⊢ ( 𝑥 ∈ On → ( 𝑦 ⊆ 𝑥 → 𝑦 ≼ 𝑥 ) )
12 10 11 syld ⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → 𝑦 ≼ 𝑥 ) )
13 12 imp ⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≼ 𝑥 )
14 13 adantlr ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≼ 𝑥 )
15 simplrr ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ≺ 𝑇 )
16 domsdomtr ⊢ ( ( 𝑦 ≼ 𝑥 ∧ 𝑥 ≺ 𝑇 ) → 𝑦 ≺ 𝑇 )
17 14 15 16 syl2anc ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ≺ 𝑇 )
18 pm2.27 ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → ( ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝑇 ) )
19 9 17 18 syl2anc ⊢ ( ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝑇 ) )
20 19 ralimdva ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑇 ) )
21 dfss3 ⊢ ( 𝑥 ⊆ 𝑇 ↔ ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑇 )
22 tskssel ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ⊆ 𝑇 ∧ 𝑥 ≺ 𝑇 ) → 𝑥 ∈ 𝑇 )
23 22 3exp ⊢ ( 𝑇 ∈ Tarski → ( 𝑥 ⊆ 𝑇 → ( 𝑥 ≺ 𝑇 → 𝑥 ∈ 𝑇 ) ) )
24 21 23 syl5bir ⊢ ( 𝑇 ∈ Tarski → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑇 → ( 𝑥 ≺ 𝑇 → 𝑥 ∈ 𝑇 ) ) )
25 24 com23 ⊢ ( 𝑇 ∈ Tarski → ( 𝑥 ≺ 𝑇 → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑇 → 𝑥 ∈ 𝑇 ) ) )
26 25 imp ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑇 → 𝑥 ∈ 𝑇 ) )
27 26 adantl ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ 𝑇 → 𝑥 ∈ 𝑇 ) )
28 20 27 syld ⊢ ( ( 𝑥 ∈ On ∧ ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 ) → 𝑥 ∈ 𝑇 ) )
29 28 ex ⊢ ( 𝑥 ∈ On → ( ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 ) → 𝑥 ∈ 𝑇 ) ) )
30 29 com23 ⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑇 ∈ Tarski ∧ 𝑦 ≺ 𝑇 ) → 𝑦 ∈ 𝑇 ) → ( ( 𝑇 ∈ Tarski ∧ 𝑥 ≺ 𝑇 ) → 𝑥 ∈ 𝑇 ) ) )
31 4 8 30 tfis3 ⊢ ( 𝐴 ∈ On → ( ( 𝑇 ∈ Tarski ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 ) )
32 31 3impib ⊢ ( ( 𝐴 ∈ On ∧ 𝑇 ∈ Tarski ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 )
33 32 3com12 ⊢ ( ( 𝑇 ∈ Tarski ∧ 𝐴 ∈ On ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 )