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	biimtrrid	⊢ ( 𝑇 ∈ 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 ∧ 𝐴 ≺ 𝑇 ) → 𝐴 ∈ 𝑇 )