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