Step | Hyp | Ref
| Expression |
1 | | inss1 4162 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
2 | 1 | sseli 3917 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) → (𝐴 ∩ 𝐵) ∈ 𝐴) |
3 | | dfon2lem4.1 |
. . . . . . . . . . . 12
⊢ 𝐴 ∈ V |
4 | | dfon2lem3 33761 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ V → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧)) |
6 | 5 | simprd 496 |
. . . . . . . . . 10
⊢
(∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧) |
7 | | eleq1 2826 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐴 ∩ 𝐵) → (𝑧 ∈ 𝑧 ↔ (𝐴 ∩ 𝐵) ∈ 𝑧)) |
8 | | eleq2 2827 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝐴 ∩ 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝑧 ↔ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))) |
9 | 7, 8 | bitrd 278 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐴 ∩ 𝐵) → (𝑧 ∈ 𝑧 ↔ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))) |
10 | 9 | notbid 318 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐴 ∩ 𝐵) → (¬ 𝑧 ∈ 𝑧 ↔ ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))) |
11 | 10 | rspccv 3558 |
. . . . . . . . . 10
⊢
(∀𝑧 ∈
𝐴 ¬ 𝑧 ∈ 𝑧 → ((𝐴 ∩ 𝐵) ∈ 𝐴 → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))) |
12 | 6, 11 | syl 17 |
. . . . . . . . 9
⊢
(∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))) |
13 | 12 | adantr 481 |
. . . . . . . 8
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ((𝐴 ∩ 𝐵) ∈ 𝐴 → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))) |
14 | 2, 13 | syl5 34 |
. . . . . . 7
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵))) |
15 | 14 | pm2.01d 189 |
. . . . . 6
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵)) |
16 | | elin 3903 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵)) |
17 | 15, 16 | sylnib 328 |
. . . . 5
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ¬ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵)) |
18 | 5 | simpld 495 |
. . . . . . . 8
⊢
(∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → Tr 𝐴) |
19 | | dfon2lem4.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
20 | | dfon2lem3 33761 |
. . . . . . . . . 10
⊢ (𝐵 ∈ V → (∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵) → (Tr 𝐵 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝑧))) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . 9
⊢
(∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵) → (Tr 𝐵 ∧ ∀𝑧 ∈ 𝐵 ¬ 𝑧 ∈ 𝑧)) |
22 | 21 | simpld 495 |
. . . . . . . 8
⊢
(∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵) → Tr 𝐵) |
23 | | trin 5201 |
. . . . . . . 8
⊢ ((Tr
𝐴 ∧ Tr 𝐵) → Tr (𝐴 ∩ 𝐵)) |
24 | 18, 22, 23 | syl2an 596 |
. . . . . . 7
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → Tr (𝐴 ∩ 𝐵)) |
25 | 3 | inex1 5241 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) ∈ V |
26 | | psseq1 4022 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 ∩ 𝐵) → (𝑥 ⊊ 𝐴 ↔ (𝐴 ∩ 𝐵) ⊊ 𝐴)) |
27 | | treq 5197 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝐴 ∩ 𝐵) → (Tr 𝑥 ↔ Tr (𝐴 ∩ 𝐵))) |
28 | 26, 27 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∩ 𝐵) → ((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∧ Tr (𝐴 ∩ 𝐵)))) |
29 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (𝑥 = (𝐴 ∩ 𝐵) → (𝑥 ∈ 𝐴 ↔ (𝐴 ∩ 𝐵) ∈ 𝐴)) |
30 | 28, 29 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑥 = (𝐴 ∩ 𝐵) → (((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ↔ (((𝐴 ∩ 𝐵) ⊊ 𝐴 ∧ Tr (𝐴 ∩ 𝐵)) → (𝐴 ∩ 𝐵) ∈ 𝐴))) |
31 | 25, 30 | spcv 3544 |
. . . . . . . 8
⊢
(∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (((𝐴 ∩ 𝐵) ⊊ 𝐴 ∧ Tr (𝐴 ∩ 𝐵)) → (𝐴 ∩ 𝐵) ∈ 𝐴)) |
32 | 31 | adantr 481 |
. . . . . . 7
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (((𝐴 ∩ 𝐵) ⊊ 𝐴 ∧ Tr (𝐴 ∩ 𝐵)) → (𝐴 ∩ 𝐵) ∈ 𝐴)) |
33 | 24, 32 | mpan2d 691 |
. . . . . 6
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ((𝐴 ∩ 𝐵) ⊊ 𝐴 → (𝐴 ∩ 𝐵) ∈ 𝐴)) |
34 | | psseq1 4022 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐴 ∩ 𝐵) → (𝑦 ⊊ 𝐵 ↔ (𝐴 ∩ 𝐵) ⊊ 𝐵)) |
35 | | treq 5197 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐴 ∩ 𝐵) → (Tr 𝑦 ↔ Tr (𝐴 ∩ 𝐵))) |
36 | 34, 35 | anbi12d 631 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 ∩ 𝐵) → ((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐵 ∧ Tr (𝐴 ∩ 𝐵)))) |
37 | | eleq1 2826 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐴 ∩ 𝐵) → (𝑦 ∈ 𝐵 ↔ (𝐴 ∩ 𝐵) ∈ 𝐵)) |
38 | 36, 37 | imbi12d 345 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 ∩ 𝐵) → (((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵) ↔ (((𝐴 ∩ 𝐵) ⊊ 𝐵 ∧ Tr (𝐴 ∩ 𝐵)) → (𝐴 ∩ 𝐵) ∈ 𝐵))) |
39 | 25, 38 | spcv 3544 |
. . . . . . . 8
⊢
(∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵) → (((𝐴 ∩ 𝐵) ⊊ 𝐵 ∧ Tr (𝐴 ∩ 𝐵)) → (𝐴 ∩ 𝐵) ∈ 𝐵)) |
40 | 39 | adantl 482 |
. . . . . . 7
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (((𝐴 ∩ 𝐵) ⊊ 𝐵 ∧ Tr (𝐴 ∩ 𝐵)) → (𝐴 ∩ 𝐵) ∈ 𝐵)) |
41 | 24, 40 | mpan2d 691 |
. . . . . 6
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ((𝐴 ∩ 𝐵) ⊊ 𝐵 → (𝐴 ∩ 𝐵) ∈ 𝐵)) |
42 | 33, 41 | anim12d 609 |
. . . . 5
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (((𝐴 ∩ 𝐵) ⊊ 𝐴 ∧ (𝐴 ∩ 𝐵) ⊊ 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵))) |
43 | 17, 42 | mtod 197 |
. . . 4
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ¬ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∧ (𝐴 ∩ 𝐵) ⊊ 𝐵)) |
44 | | ianor 979 |
. . . 4
⊢ (¬
((𝐴 ∩ 𝐵) ⊊ 𝐴 ∧ (𝐴 ∩ 𝐵) ⊊ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ ¬ (𝐴 ∩ 𝐵) ⊊ 𝐵)) |
45 | 43, 44 | sylib 217 |
. . 3
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (¬ (𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ ¬ (𝐴 ∩ 𝐵) ⊊ 𝐵)) |
46 | | sspss 4034 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)) |
47 | 1, 46 | mpbi 229 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴) |
48 | | inss2 4163 |
. . . . 5
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
49 | | sspss 4034 |
. . . . 5
⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐵 ↔ ((𝐴 ∩ 𝐵) ⊊ 𝐵 ∨ (𝐴 ∩ 𝐵) = 𝐵)) |
50 | 48, 49 | mpbi 229 |
. . . 4
⊢ ((𝐴 ∩ 𝐵) ⊊ 𝐵 ∨ (𝐴 ∩ 𝐵) = 𝐵) |
51 | | orel1 886 |
. . . . . 6
⊢ (¬
(𝐴 ∩ 𝐵) ⊊ 𝐴 → (((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴) → (𝐴 ∩ 𝐵) = 𝐴)) |
52 | | orc 864 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) = 𝐴 → ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵)) |
53 | 51, 52 | syl6 35 |
. . . . 5
⊢ (¬
(𝐴 ∩ 𝐵) ⊊ 𝐴 → (((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴) → ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵))) |
54 | | orel1 886 |
. . . . . 6
⊢ (¬
(𝐴 ∩ 𝐵) ⊊ 𝐵 → (((𝐴 ∩ 𝐵) ⊊ 𝐵 ∨ (𝐴 ∩ 𝐵) = 𝐵) → (𝐴 ∩ 𝐵) = 𝐵)) |
55 | | olc 865 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) = 𝐵 → ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵)) |
56 | 54, 55 | syl6 35 |
. . . . 5
⊢ (¬
(𝐴 ∩ 𝐵) ⊊ 𝐵 → (((𝐴 ∩ 𝐵) ⊊ 𝐵 ∨ (𝐴 ∩ 𝐵) = 𝐵) → ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵))) |
57 | 53, 56 | jaoa 953 |
. . . 4
⊢ ((¬
(𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ ¬ (𝐴 ∩ 𝐵) ⊊ 𝐵) → ((((𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴) ∧ ((𝐴 ∩ 𝐵) ⊊ 𝐵 ∨ (𝐴 ∩ 𝐵) = 𝐵)) → ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵))) |
58 | 47, 50, 57 | mp2ani 695 |
. . 3
⊢ ((¬
(𝐴 ∩ 𝐵) ⊊ 𝐴 ∨ ¬ (𝐴 ∩ 𝐵) ⊊ 𝐵) → ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵)) |
59 | 45, 58 | syl 17 |
. 2
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵)) |
60 | | df-ss 3904 |
. . 3
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
61 | | sseqin2 4149 |
. . 3
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐴 ∩ 𝐵) = 𝐵) |
62 | 60, 61 | orbi12i 912 |
. 2
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ ((𝐴 ∩ 𝐵) = 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐵)) |
63 | 59, 62 | sylibr 233 |
1
⊢
((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |