tskord

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

		Ref	Expression
	Assertion	tskord	$⊢ (T \in Tarski \land A \in On \land A ≺ T) \to A \in T$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = y \to (x ≺ T \leftrightarrow y ≺ T)$
2	1	anbi2d	$⊢ x = y \to ((T \in Tarski \land x ≺ T) \leftrightarrow (T \in Tarski \land y ≺ T))$
3		eleq1	$⊢ x = y \to (x \in T \leftrightarrow y \in T)$
4	2 3	imbi12d	$⊢ x = y \to (((T \in Tarski \land x ≺ T) \to x \in T) \leftrightarrow ((T \in Tarski \land y ≺ T) \to y \in T))$
5		breq1	$⊢ x = A \to (x ≺ T \leftrightarrow A ≺ T)$
6	5	anbi2d	$⊢ x = A \to ((T \in Tarski \land x ≺ T) \leftrightarrow (T \in Tarski \land A ≺ T))$
7		eleq1	$⊢ x = A \to (x \in T \leftrightarrow A \in T)$
8	6 7	imbi12d	$⊢ x = A \to (((T \in Tarski \land x ≺ T) \to x \in T) \leftrightarrow ((T \in Tarski \land A ≺ T) \to A \in T))$
9		simplrl	$⊢ ((x \in On \land (T \in Tarski \land x ≺ T)) \land y \in x) \to T \in Tarski$
10		onelss	$⊢ x \in On \to (y \in x \to y \subseteq x)$
11		ssdomg	$⊢ x \in On \to (y \subseteq x \to y ≼ x)$
12	10 11	syld	$⊢ x \in On \to (y \in x \to y ≼ x)$
13	12	imp	$⊢ (x \in On \land y \in x) \to y ≼ x$
14	13	adantlr	$⊢ ((x \in On \land (T \in Tarski \land x ≺ T)) \land y \in x) \to y ≼ x$
15		simplrr	$⊢ ((x \in On \land (T \in Tarski \land x ≺ T)) \land y \in x) \to x ≺ T$
16		domsdomtr	$⊢ (y ≼ x \land x ≺ T) \to y ≺ T$
17	14 15 16	syl2anc	$⊢ ((x \in On \land (T \in Tarski \land x ≺ T)) \land y \in x) \to y ≺ T$
18		pm2.27	$⊢ (T \in Tarski \land y ≺ T) \to (((T \in Tarski \land y ≺ T) \to y \in T) \to y \in T)$
19	9 17 18	syl2anc	$⊢ ((x \in On \land (T \in Tarski \land x ≺ T)) \land y \in x) \to (((T \in Tarski \land y ≺ T) \to y \in T) \to y \in T)$
20	19	ralimdva	$⊢ (x \in On \land (T \in Tarski \land x ≺ T)) \to (\forall y \in x ((T \in Tarski \land y ≺ T) \to y \in T) \to \forall y \in x y \in T)$
21		dfss3	$⊢ x \subseteq T \leftrightarrow \forall y \in x y \in T$
22		tskssel	$⊢ (T \in Tarski \land x \subseteq T \land x ≺ T) \to x \in T$
23	22	3exp	$⊢ T \in Tarski \to (x \subseteq T \to (x ≺ T \to x \in T))$
24	21 23	syl5bir	$⊢ T \in Tarski \to (\forall y \in x y \in T \to (x ≺ T \to x \in T))$
25	24	com23	$⊢ T \in Tarski \to (x ≺ T \to (\forall y \in x y \in T \to x \in T))$
26	25	imp	$⊢ (T \in Tarski \land x ≺ T) \to (\forall y \in x y \in T \to x \in T)$
27	26	adantl	$⊢ (x \in On \land (T \in Tarski \land x ≺ T)) \to (\forall y \in x y \in T \to x \in T)$
28	20 27	syld	$⊢ (x \in On \land (T \in Tarski \land x ≺ T)) \to (\forall y \in x ((T \in Tarski \land y ≺ T) \to y \in T) \to x \in T)$
29	28	ex	$⊢ x \in On \to ((T \in Tarski \land x ≺ T) \to (\forall y \in x ((T \in Tarski \land y ≺ T) \to y \in T) \to x \in T))$
30	29	com23	$⊢ x \in On \to (\forall y \in x ((T \in Tarski \land y ≺ T) \to y \in T) \to ((T \in Tarski \land x ≺ T) \to x \in T))$
31	4 8 30	tfis3	$⊢ A \in On \to ((T \in Tarski \land A ≺ T) \to A \in T)$
32	31	3impib	$⊢ (A \in On \land T \in Tarski \land A ≺ T) \to A \in T$
33	32	3com12	$⊢ (T \in Tarski \land A \in On \land A ≺ T) \to A \in T$

Metamath Proof Explorer

Theorem tskord

Proof