This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑦 ) → 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴 ) )