dfon2lem5

Description: Lemma for dfon2 . Two sets satisfying the new definition also satisfy trichotomy with respect to e. . (Contributed by Scott Fenton, 25-Feb-2011)

	Ref	Expression
Hypotheses	dfon2lem5.1	$⊢ A \in V$
	dfon2lem5.2	$⊢ B \in V$
Assertion	dfon2lem5	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to (A \in B \lor A = B \lor B \in A)$

Proof

Step	Hyp	Ref	Expression
1		dfon2lem5.1	$⊢ A \in V$
2		dfon2lem5.2	$⊢ B \in V$
3	1 2	dfon2lem4	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to (A \subseteq B \lor B \subseteq A)$
4		dfpss2	$⊢ A \subset B \leftrightarrow (A \subseteq B \land \neg A = B)$
5		dfpss2	$⊢ B \subset A \leftrightarrow (B \subseteq A \land \neg B = A)$
6		eqcom	$⊢ B = A \leftrightarrow A = B$
7	6	notbii	$⊢ \neg B = A \leftrightarrow \neg A = B$
8	7	anbi2i	$⊢ (B \subseteq A \land \neg B = A) \leftrightarrow (B \subseteq A \land \neg A = B)$
9	5 8	bitri	$⊢ B \subset A \leftrightarrow (B \subseteq A \land \neg A = B)$
10	4 9	orbi12i	$⊢ (A \subset B \lor B \subset A) \leftrightarrow ((A \subseteq B \land \neg A = B) \lor (B \subseteq A \land \neg A = B))$
11		andir	$⊢ ((A \subseteq B \lor B \subseteq A) \land \neg A = B) \leftrightarrow ((A \subseteq B \land \neg A = B) \lor (B \subseteq A \land \neg A = B))$
12	10 11	bitr4i	$⊢ (A \subset B \lor B \subset A) \leftrightarrow ((A \subseteq B \lor B \subseteq A) \land \neg A = B)$
13		orcom	$⊢ (A \subset B \lor B \subset A) \leftrightarrow (B \subset A \lor A \subset B)$
14		dfon2lem3	$⊢ B \in V \to (\forall y ((y \subset B \land Tr y) \to y \in B) \to (Tr B \land \forall z \in B \neg z \in z))$
15	2 14	ax-mp	$⊢ \forall y ((y \subset B \land Tr y) \to y \in B) \to (Tr B \land \forall z \in B \neg z \in z)$
16	15	simpld	$⊢ \forall y ((y \subset B \land Tr y) \to y \in B) \to Tr B$
17		psseq1	$⊢ x = B \to (x \subset A \leftrightarrow B \subset A)$
18		treq	$⊢ x = B \to (Tr x \leftrightarrow Tr B)$
19	17 18	anbi12d	$⊢ x = B \to ((x \subset A \land Tr x) \leftrightarrow (B \subset A \land Tr B))$
20		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
21	19 20	imbi12d	$⊢ x = B \to (((x \subset A \land Tr x) \to x \in A) \leftrightarrow ((B \subset A \land Tr B) \to B \in A))$
22	2 21	spcv	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to ((B \subset A \land Tr B) \to B \in A)$
23	22	expcomd	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (Tr B \to (B \subset A \to B \in A))$
24	23	imp	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land Tr B) \to (B \subset A \to B \in A)$
25	16 24	sylan2	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to (B \subset A \to B \in A)$
26		dfon2lem3	$⊢ A \in V \to (\forall x ((x \subset A \land Tr x) \to x \in A) \to (Tr A \land \forall z \in A \neg z \in z))$
27	1 26	ax-mp	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (Tr A \land \forall z \in A \neg z \in z)$
28	27	simpld	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to Tr A$
29		psseq1	$⊢ y = A \to (y \subset B \leftrightarrow A \subset B)$
30		treq	$⊢ y = A \to (Tr y \leftrightarrow Tr A)$
31	29 30	anbi12d	$⊢ y = A \to ((y \subset B \land Tr y) \leftrightarrow (A \subset B \land Tr A))$
32		eleq1	$⊢ y = A \to (y \in B \leftrightarrow A \in B)$
33	31 32	imbi12d	$⊢ y = A \to (((y \subset B \land Tr y) \to y \in B) \leftrightarrow ((A \subset B \land Tr A) \to A \in B))$
34	1 33	spcv	$⊢ \forall y ((y \subset B \land Tr y) \to y \in B) \to ((A \subset B \land Tr A) \to A \in B)$
35	34	expcomd	$⊢ \forall y ((y \subset B \land Tr y) \to y \in B) \to (Tr A \to (A \subset B \to A \in B))$
36	28 35	mpan9	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to (A \subset B \to A \in B)$
37	25 36	orim12d	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to ((B \subset A \lor A \subset B) \to (B \in A \lor A \in B))$
38	13 37	biimtrid	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to ((A \subset B \lor B \subset A) \to (B \in A \lor A \in B))$
39	12 38	biimtrrid	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to (((A \subseteq B \lor B \subseteq A) \land \neg A = B) \to (B \in A \lor A \in B))$
40	3 39	mpand	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to (\neg A = B \to (B \in A \lor A \in B))$
41		3orrot	$⊢ (A \in B \lor A = B \lor B \in A) \leftrightarrow (A = B \lor B \in A \lor A \in B)$
42		3orass	$⊢ (A = B \lor B \in A \lor A \in B) \leftrightarrow (A = B \lor (B \in A \lor A \in B))$
43		df-or	$⊢ (A = B \lor (B \in A \lor A \in B)) \leftrightarrow (\neg A = B \to (B \in A \lor A \in B))$
44	42 43	bitri	$⊢ (A = B \lor B \in A \lor A \in B) \leftrightarrow (\neg A = B \to (B \in A \lor A \in B))$
45	41 44	bitri	$⊢ (A \in B \lor A = B \lor B \in A) \leftrightarrow (\neg A = B \to (B \in A \lor A \in B))$
46	40 45	sylibr	$⊢ (\forall x ((x \subset A \land Tr x) \to x \in A) \land \forall y ((y \subset B \land Tr y) \to y \in B)) \to (A \in B \lor A = B \lor B \in A)$

Metamath Proof Explorer

Theorem dfon2lem5

Proof