tz7.7

Description: A transitive class belongs to an ordinal class iff it is strictly included in it. Proposition 7.7 of TakeutiZaring p. 37. (Contributed by NM, 5-May-1994)

		Ref	Expression
	Assertion	tz7.7	$⊢ (Ord A \land Tr B) \to (B \in A \leftrightarrow (B \subseteq A \land B \neq A))$

Proof

Step	Hyp	Ref	Expression
1		ordtr	$⊢ Ord A \to Tr A$
2		ordfr	$⊢ Ord A \to E Fr A$
3		tz7.2	$⊢ (Tr A \land E Fr A \land B \in A) \to (B \subseteq A \land B \neq A)$
4	3	3exp	$⊢ Tr A \to (E Fr A \to (B \in A \to (B \subseteq A \land B \neq A)))$
5	1 2 4	sylc	$⊢ Ord A \to (B \in A \to (B \subseteq A \land B \neq A))$
6	5	adantr	$⊢ (Ord A \land Tr B) \to (B \in A \to (B \subseteq A \land B \neq A))$
7		pssdifn0	$⊢ (B \subseteq A \land B \neq A) \to A ∖ B \neq \emptyset$
8		difss	$⊢ A ∖ B \subseteq A$
9		tz7.5	$⊢ (Ord A \land A ∖ B \subseteq A \land A ∖ B \neq \emptyset) \to \exists x \in (A ∖ B) (A ∖ B) \cap x = \emptyset$
10	8 9	mp3an2	$⊢ (Ord A \land A ∖ B \neq \emptyset) \to \exists x \in (A ∖ B) (A ∖ B) \cap x = \emptyset$
11		eldifi	$⊢ x \in (A ∖ B) \to x \in A$
12		trss	$⊢ Tr A \to (x \in A \to x \subseteq A)$
13		difin0ss	$⊢ (A ∖ B) \cap x = \emptyset \to (x \subseteq A \to x \subseteq B)$
14	13	com12	$⊢ x \subseteq A \to ((A ∖ B) \cap x = \emptyset \to x \subseteq B)$
15	11 12 14	syl56	$⊢ Tr A \to (x \in (A ∖ B) \to ((A ∖ B) \cap x = \emptyset \to x \subseteq B))$
16	1 15	syl	$⊢ Ord A \to (x \in (A ∖ B) \to ((A ∖ B) \cap x = \emptyset \to x \subseteq B))$
17	16	ad2antrr	$⊢ ((Ord A \land Tr B) \land B \subseteq A) \to (x \in (A ∖ B) \to ((A ∖ B) \cap x = \emptyset \to x \subseteq B))$
18	17	imp32	$⊢ (((Ord A \land Tr B) \land B \subseteq A) \land (x \in (A ∖ B) \land (A ∖ B) \cap x = \emptyset)) \to x \subseteq B$
19		eleq1w	$⊢ y = x \to (y \in B \leftrightarrow x \in B)$
20	19	biimpcd	$⊢ y \in B \to (y = x \to x \in B)$
21		eldifn	$⊢ x \in (A ∖ B) \to \neg x \in B$
22	20 21	nsyli	$⊢ y \in B \to (x \in (A ∖ B) \to \neg y = x)$
23	22	imp	$⊢ (y \in B \land x \in (A ∖ B)) \to \neg y = x$
24	23	adantll	$⊢ ((B \subseteq A \land y \in B) \land x \in (A ∖ B)) \to \neg y = x$
25	24	adantl	$⊢ ((Ord A \land Tr B) \land ((B \subseteq A \land y \in B) \land x \in (A ∖ B))) \to \neg y = x$
26		trel	$⊢ Tr B \to ((x \in y \land y \in B) \to x \in B)$
27	26	expcomd	$⊢ Tr B \to (y \in B \to (x \in y \to x \in B))$
28	27	imp	$⊢ (Tr B \land y \in B) \to (x \in y \to x \in B)$
29	28 21	nsyli	$⊢ (Tr B \land y \in B) \to (x \in (A ∖ B) \to \neg x \in y)$
30	29	ex	$⊢ Tr B \to (y \in B \to (x \in (A ∖ B) \to \neg x \in y))$
31	30	adantld	$⊢ Tr B \to ((B \subseteq A \land y \in B) \to (x \in (A ∖ B) \to \neg x \in y))$
32	31	imp32	$⊢ (Tr B \land ((B \subseteq A \land y \in B) \land x \in (A ∖ B))) \to \neg x \in y$
33	32	adantll	$⊢ ((Ord A \land Tr B) \land ((B \subseteq A \land y \in B) \land x \in (A ∖ B))) \to \neg x \in y$
34		ordwe	$⊢ Ord A \to E We A$
35		ssel2	$⊢ (B \subseteq A \land y \in B) \to y \in A$
36	35 11	anim12i	$⊢ ((B \subseteq A \land y \in B) \land x \in (A ∖ B)) \to (y \in A \land x \in A)$
37		wecmpep	$⊢ (E We A \land (y \in A \land x \in A)) \to (y \in x \lor y = x \lor x \in y)$
38	34 36 37	syl2an	$⊢ (Ord A \land ((B \subseteq A \land y \in B) \land x \in (A ∖ B))) \to (y \in x \lor y = x \lor x \in y)$
39	38	adantlr	$⊢ ((Ord A \land Tr B) \land ((B \subseteq A \land y \in B) \land x \in (A ∖ B))) \to (y \in x \lor y = x \lor x \in y)$
40	25 33 39	ecase23d	$⊢ ((Ord A \land Tr B) \land ((B \subseteq A \land y \in B) \land x \in (A ∖ B))) \to y \in x$
41	40	exp44	$⊢ (Ord A \land Tr B) \to (B \subseteq A \to (y \in B \to (x \in (A ∖ B) \to y \in x)))$
42	41	com34	$⊢ (Ord A \land Tr B) \to (B \subseteq A \to (x \in (A ∖ B) \to (y \in B \to y \in x)))$
43	42	imp31	$⊢ (((Ord A \land Tr B) \land B \subseteq A) \land x \in (A ∖ B)) \to (y \in B \to y \in x)$
44	43	ssrdv	$⊢ (((Ord A \land Tr B) \land B \subseteq A) \land x \in (A ∖ B)) \to B \subseteq x$
45	44	adantrr	$⊢ (((Ord A \land Tr B) \land B \subseteq A) \land (x \in (A ∖ B) \land (A ∖ B) \cap x = \emptyset)) \to B \subseteq x$
46	18 45	eqssd	$⊢ (((Ord A \land Tr B) \land B \subseteq A) \land (x \in (A ∖ B) \land (A ∖ B) \cap x = \emptyset)) \to x = B$
47	11	ad2antrl	$⊢ (((Ord A \land Tr B) \land B \subseteq A) \land (x \in (A ∖ B) \land (A ∖ B) \cap x = \emptyset)) \to x \in A$
48	46 47	eqeltrrd	$⊢ (((Ord A \land Tr B) \land B \subseteq A) \land (x \in (A ∖ B) \land (A ∖ B) \cap x = \emptyset)) \to B \in A$
49	48	rexlimdvaa	$⊢ ((Ord A \land Tr B) \land B \subseteq A) \to (\exists x \in (A ∖ B) (A ∖ B) \cap x = \emptyset \to B \in A)$
50	10 49	syl5	$⊢ ((Ord A \land Tr B) \land B \subseteq A) \to ((Ord A \land A ∖ B \neq \emptyset) \to B \in A)$
51	50	exp4b	$⊢ (Ord A \land Tr B) \to (B \subseteq A \to (Ord A \to (A ∖ B \neq \emptyset \to B \in A)))$
52	51	com23	$⊢ (Ord A \land Tr B) \to (Ord A \to (B \subseteq A \to (A ∖ B \neq \emptyset \to B \in A)))$
53	52	adantrd	$⊢ (Ord A \land Tr B) \to ((Ord A \land Tr B) \to (B \subseteq A \to (A ∖ B \neq \emptyset \to B \in A)))$
54	53	pm2.43i	$⊢ (Ord A \land Tr B) \to (B \subseteq A \to (A ∖ B \neq \emptyset \to B \in A))$
55	7 54	syl7	$⊢ (Ord A \land Tr B) \to (B \subseteq A \to ((B \subseteq A \land B \neq A) \to B \in A))$
56	55	exp4a	$⊢ (Ord A \land Tr B) \to (B \subseteq A \to (B \subseteq A \to (B \neq A \to B \in A)))$
57	56	pm2.43d	$⊢ (Ord A \land Tr B) \to (B \subseteq A \to (B \neq A \to B \in A))$
58	57	impd	$⊢ (Ord A \land Tr B) \to ((B \subseteq A \land B \neq A) \to B \in A)$
59	6 58	impbid	$⊢ (Ord A \land Tr B) \to (B \in A \leftrightarrow (B \subseteq A \land B \neq A))$

Metamath Proof Explorer

Theorem tz7.7

Proof