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 df-ss ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = 𝐴 )
61 sseqin2 ( 𝐵𝐴 ↔ ( 𝐴𝐵 ) = 𝐵 )
62 60 61 orbi12i ( ( 𝐴𝐵𝐵𝐴 ) ↔ ( ( 𝐴𝐵 ) = 𝐴 ∨ ( 𝐴𝐵 ) = 𝐵 ) )
63 59 62 sylibr ( ( ∀ 𝑥 ( ( 𝑥𝐴 ∧ Tr 𝑥 ) → 𝑥𝐴 ) ∧ ∀ 𝑦 ( ( 𝑦𝐵 ∧ Tr 𝑦 ) → 𝑦𝐵 ) ) → ( 𝐴𝐵𝐵𝐴 ) )