dfon2lem4

Description: Lemma for dfon2 . If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011)

	Ref	Expression
Hypotheses	dfon2lem4.1	$⊢ A \in V$
	dfon2lem4.2	$⊢ B \in V$
Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		dfon2lem4.1	$⊢ A \in V$
2		dfon2lem4.2	$⊢ B \in V$
3		inss1	$⊢ A \cap B \subseteq A$
4	3	sseli	$⊢ A \cap B \in (A \cap B) \to A \cap B \in A$
5		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))$
6	1 5	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)$
7	6	simprd	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to \forall z \in A \neg z \in z$
8		eleq1	$⊢ z = A \cap B \to (z \in z \leftrightarrow A \cap B \in z)$
9		eleq2	$⊢ z = A \cap B \to (A \cap B \in z \leftrightarrow A \cap B \in (A \cap B))$
10	8 9	bitrd	$⊢ z = A \cap B \to (z \in z \leftrightarrow A \cap B \in (A \cap B))$
11	10	notbid	$⊢ z = A \cap B \to (\neg z \in z \leftrightarrow \neg A \cap B \in (A \cap B))$
12	11	rspccv	$⊢ \forall z \in A \neg z \in z \to (A \cap B \in A \to \neg A \cap B \in (A \cap B))$
13	7 12	syl	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to (A \cap B \in A \to \neg A \cap B \in (A \cap B))$
14	13	adantr	$⊢ (\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 \cap B \in A \to \neg A \cap B \in (A \cap B))$
15	4 14	syl5	$⊢ (\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 \cap B \in (A \cap B) \to \neg A \cap B \in (A \cap B))$
16	15	pm2.01d	$⊢ (\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 \cap B \in (A \cap B)$
17		elin	$⊢ A \cap B \in (A \cap B) \leftrightarrow (A \cap B \in A \land A \cap B \in B)$
18	16 17	sylnib	$⊢ (\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 \cap B \in A \land A \cap B \in B)$
19	6	simpld	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to Tr A$
20		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))$
21	2 20	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)$
22	21	simpld	$⊢ \forall y ((y \subset B \land Tr y) \to y \in B) \to Tr B$
23		trin	$⊢ (Tr A \land Tr B) \to Tr (A \cap B)$
24	19 22 23	syl2an	$⊢ (\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 Tr (A \cap B)$
25	1	inex1	$⊢ A \cap B \in V$
26		psseq1	$⊢ x = A \cap B \to (x \subset A \leftrightarrow A \cap B \subset A)$
27		treq	$⊢ x = A \cap B \to (Tr x \leftrightarrow Tr (A \cap B))$
28	26 27	anbi12d	$⊢ x = A \cap B \to ((x \subset A \land Tr x) \leftrightarrow (A \cap B \subset A \land Tr (A \cap B)))$
29		eleq1	$⊢ x = A \cap B \to (x \in A \leftrightarrow A \cap B \in A)$
30	28 29	imbi12d	$⊢ x = A \cap B \to (((x \subset A \land Tr x) \to x \in A) \leftrightarrow ((A \cap B \subset A \land Tr (A \cap B)) \to A \cap B \in A))$
31	25 30	spcv	$⊢ \forall x ((x \subset A \land Tr x) \to x \in A) \to ((A \cap B \subset A \land Tr (A \cap B)) \to A \cap B \in A)$
32	31	adantr	$⊢ (\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 \cap B \subset A \land Tr (A \cap B)) \to A \cap B \in A)$
33	24 32	mpan2d	$⊢ (\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 \cap B \subset A \to A \cap B \in A)$
34		psseq1	$⊢ y = A \cap B \to (y \subset B \leftrightarrow A \cap B \subset B)$
35		treq	$⊢ y = A \cap B \to (Tr y \leftrightarrow Tr (A \cap B))$
36	34 35	anbi12d	$⊢ y = A \cap B \to ((y \subset B \land Tr y) \leftrightarrow (A \cap B \subset B \land Tr (A \cap B)))$
37		eleq1	$⊢ y = A \cap B \to (y \in B \leftrightarrow A \cap B \in B)$
38	36 37	imbi12d	$⊢ y = A \cap B \to (((y \subset B \land Tr y) \to y \in B) \leftrightarrow ((A \cap B \subset B \land Tr (A \cap B)) \to A \cap B \in B))$
39	25 38	spcv	$⊢ \forall y ((y \subset B \land Tr y) \to y \in B) \to ((A \cap B \subset B \land Tr (A \cap B)) \to A \cap B \in B)$
40	39	adantl	$⊢ (\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 \cap B \subset B \land Tr (A \cap B)) \to A \cap B \in B)$
41	24 40	mpan2d	$⊢ (\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 \cap B \subset B \to A \cap B \in B)$
42	33 41	anim12d	$⊢ (\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 \cap B \subset A \land A \cap B \subset B) \to (A \cap B \in A \land A \cap B \in B))$
43	18 42	mtod	$⊢ (\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 \cap B \subset A \land A \cap B \subset B)$
44		ianor	$⊢ \neg (A \cap B \subset A \land A \cap B \subset B) \leftrightarrow (\neg A \cap B \subset A \lor \neg A \cap B \subset B)$
45	43 44	sylib	$⊢ (\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 \cap B \subset A \lor \neg A \cap B \subset B)$
46		sspss	$⊢ A \cap B \subseteq A \leftrightarrow (A \cap B \subset A \lor A \cap B = A)$
47	3 46	mpbi	$⊢ (A \cap B \subset A \lor A \cap B = A)$
48		inss2	$⊢ A \cap B \subseteq B$
49		sspss	$⊢ A \cap B \subseteq B \leftrightarrow (A \cap B \subset B \lor A \cap B = B)$
50	48 49	mpbi	$⊢ (A \cap B \subset B \lor A \cap B = B)$
51		orel1	$⊢ \neg A \cap B \subset A \to ((A \cap B \subset A \lor A \cap B = A) \to A \cap B = A)$
52		orc	$⊢ A \cap B = A \to (A \cap B = A \lor A \cap B = B)$
53	51 52	syl6	$⊢ \neg A \cap B \subset A \to ((A \cap B \subset A \lor A \cap B = A) \to (A \cap B = A \lor A \cap B = B))$
54		orel1	$⊢ \neg A \cap B \subset B \to ((A \cap B \subset B \lor A \cap B = B) \to A \cap B = B)$
55		olc	$⊢ A \cap B = B \to (A \cap B = A \lor A \cap B = B)$
56	54 55	syl6	$⊢ \neg A \cap B \subset B \to ((A \cap B \subset B \lor A \cap B = B) \to (A \cap B = A \lor A \cap B = B))$
57	53 56	jaoa	$⊢ (\neg A \cap B \subset A \lor \neg A \cap B \subset B) \to (((A \cap B \subset A \lor A \cap B = A) \land (A \cap B \subset B \lor A \cap B = B)) \to (A \cap B = A \lor A \cap B = B))$
58	47 50 57	mp2ani	$⊢ (\neg A \cap B \subset A \lor \neg A \cap B \subset B) \to (A \cap B = A \lor A \cap B = B)$
59	45 58	syl	$⊢ (\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 \cap B = A \lor A \cap B = B)$
60		df-ss	$⊢ A \subseteq B \leftrightarrow A \cap B = A$
61		sseqin2	$⊢ B \subseteq A \leftrightarrow A \cap B = B$
62	60 61	orbi12i	$⊢ (A \subseteq B \lor B \subseteq A) \leftrightarrow (A \cap B = A \lor A \cap B = B)$
63	59 62	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 \subseteq B \lor B \subseteq A)$

Metamath Proof Explorer

Theorem dfon2lem4

Proof