Theorem 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	⊢ 𝐴 ∈ V
	dfon2lem4.2	⊢ 𝐵 ∈ V
Assertion	dfon2lem4	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfon2lem4.1	⊢ 𝐴 ∈ V
2		dfon2lem4.2	⊢ 𝐵 ∈ V
3		inss1	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴
4	3	sseli	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 )
5		dfon2lem3	⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) ) )
6	1 5	ax-mp	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( Tr 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 ) )
7	6	simprd	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 )
8		eleq1	⊢ ( 𝑧 = ( 𝐴 ∩ 𝐵 ) → ( 𝑧 ∈ 𝑧 ↔ ( 𝐴 ∩ 𝐵 ) ∈ 𝑧 ) )
9		eleq2	⊢ ( 𝑧 = ( 𝐴 ∩ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑧 ↔ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
10	8 9	bitrd	⊢ ( 𝑧 = ( 𝐴 ∩ 𝐵 ) → ( 𝑧 ∈ 𝑧 ↔ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
11	10	notbid	⊢ ( 𝑧 = ( 𝐴 ∩ 𝐵 ) → ( ¬ 𝑧 ∈ 𝑧 ↔ ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
12	11	rspccv	⊢ ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧 → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 → ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
13	7 12	syl	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 → ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
14	13	adantr	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 → ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
15	4 14	syl5	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) → ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ) )
16	15	pm2.01d	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ¬ ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) )
17		elin	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) )
18	16 17	sylnib	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ¬ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) )
19	6	simpld	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → Tr 𝐴 )
20		dfon2lem3	⊢ ( 𝐵 ∈ V → ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → ( Tr 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝑧 ) ) )
21	2 20	ax-mp	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → ( Tr 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝑧 ) )
22	21	simpld	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → Tr 𝐵 )
23		trin	⊢ ( ( Tr 𝐴 ∧ Tr 𝐵 ) → Tr ( 𝐴 ∩ 𝐵 ) )
24	19 22 23	syl2an	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → Tr ( 𝐴 ∩ 𝐵 ) )
25	1	inex1	⊢ ( 𝐴 ∩ 𝐵 ) ∈ V
26		psseq1	⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) → ( 𝑥 ⊊ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ) )
27		treq	⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) → ( Tr 𝑥 ↔ Tr ( 𝐴 ∩ 𝐵 ) ) )
28	26 27	anbi12d	⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) → ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) ) )
29		eleq1	⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) → ( 𝑥 ∈ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ) )
30	28 29	imbi12d	⊢ ( 𝑥 = ( 𝐴 ∩ 𝐵 ) → ( ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ) ) )
31	25 30	spcv	⊢ ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ) )
32	31	adantr	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ) )
33	24 32	mpan2d	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ) )
34		psseq1	⊢ ( 𝑦 = ( 𝐴 ∩ 𝐵 ) → ( 𝑦 ⊊ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) )
35		treq	⊢ ( 𝑦 = ( 𝐴 ∩ 𝐵 ) → ( Tr 𝑦 ↔ Tr ( 𝐴 ∩ 𝐵 ) ) )
36	34 35	anbi12d	⊢ ( 𝑦 = ( 𝐴 ∩ 𝐵 ) → ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) ) )
37		eleq1	⊢ ( 𝑦 = ( 𝐴 ∩ 𝐵 ) → ( 𝑦 ∈ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) )
38	36 37	imbi12d	⊢ ( 𝑦 = ( 𝐴 ∩ 𝐵 ) → ( ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ↔ ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) ) )
39	25 38	spcv	⊢ ( ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) )
40	39	adantl	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∧ Tr ( 𝐴 ∩ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) )
41	24 40	mpan2d	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 → ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) )
42	33 41	anim12d	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ∈ 𝐵 ) ) )
43	18 42	mtod	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ¬ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) )
44		ianor	⊢ ( ¬ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∧ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) ↔ ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) )
45	43 44	sylib	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) )
46		sspss	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) )
47	3 46	mpbi	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
48		inss2	⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
49		sspss	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) )
50	48 49	mpbi	⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
51		orel1	⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) → ( 𝐴 ∩ 𝐵 ) = 𝐴 ) )
52		orc	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) )
53	51 52	syl6	⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) ) )
54		orel1	⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) → ( 𝐴 ∩ 𝐵 ) = 𝐵 ) )
55		olc	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐵 → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) )
56	54 55	syl6	⊢ ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) ) )
57	53 56	jaoa	⊢ ( ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) → ( ( ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐴 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) ) )
58	47 50 57	mp2ani	⊢ ( ( ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐴 ∨ ¬ ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) )
59	45 58	syl	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) )
60		dfss2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )
61		sseqin2	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
62	60 61	orbi12i	⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) ↔ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ∨ ( 𝐴 ∩ 𝐵 ) = 𝐵 ) )
63	59 62	sylibr	⊢ ( ( ∀ 𝑥 ( ( 𝑥 ⊊ 𝐴 ∧ Tr 𝑥 ) → 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦 ⊊ 𝐵 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )