Step | Hyp | Ref
| Expression |
1 | | simp2 1055 |
. 2
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) → 𝐴 ≠ ∅) |
2 | | simp1 1054 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) → 𝐴 ∈ dom
card) |
3 | | snfi 7923 |
. . . . 5
⊢ {∅}
∈ Fin |
4 | | finnum 8657 |
. . . . 5
⊢
({∅} ∈ Fin → {∅} ∈ dom card) |
5 | 3, 4 | ax-mp 5 |
. . . 4
⊢ {∅}
∈ dom card |
6 | | unnum 8905 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ {∅}
∈ dom card) → (𝐴
∪ {∅}) ∈ dom card) |
7 | 2, 5, 6 | sylancl 693 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) → (𝐴 ∪ {∅}) ∈ dom
card) |
8 | | uncom 3719 |
. . . . . . . . 9
⊢ (𝐴 ∪ {∅}) = ({∅}
∪ 𝐴) |
9 | 8 | sseq2i 3593 |
. . . . . . . 8
⊢ (𝑤 ⊆ (𝐴 ∪ {∅}) ↔ 𝑤 ⊆ ({∅} ∪ 𝐴)) |
10 | | ssundif 4004 |
. . . . . . . 8
⊢ (𝑤 ⊆ ({∅} ∪ 𝐴) ↔ (𝑤 ∖ {∅}) ⊆ 𝐴) |
11 | 9, 10 | bitri 263 |
. . . . . . 7
⊢ (𝑤 ⊆ (𝐴 ∪ {∅}) ↔ (𝑤 ∖ {∅}) ⊆ 𝐴) |
12 | | difss 3699 |
. . . . . . . . 9
⊢ (𝑤 ∖ {∅}) ⊆
𝑤 |
13 | | soss 4977 |
. . . . . . . . 9
⊢ ((𝑤 ∖ {∅}) ⊆
𝑤 → (
[⊊] Or 𝑤
→ [⊊] Or (𝑤 ∖ {∅}))) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢ (
[⊊] Or 𝑤
→ [⊊] Or (𝑤 ∖ {∅})) |
15 | | ssdif0 3896 |
. . . . . . . . . . 11
⊢ (𝑤 ⊆ {∅} ↔ (𝑤 ∖ {∅}) =
∅) |
16 | | uni0b 4399 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑤 =
∅ ↔ 𝑤 ⊆
{∅}) |
17 | 16 | biimpri 217 |
. . . . . . . . . . . 12
⊢ (𝑤 ⊆ {∅} → ∪ 𝑤 =
∅) |
18 | 17 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑤 ⊆ {∅} → (∪ 𝑤
∈ (𝐴 ∪ {∅})
↔ ∅ ∈ (𝐴
∪ {∅}))) |
19 | 15, 18 | sylbir 224 |
. . . . . . . . . 10
⊢ ((𝑤 ∖ {∅}) = ∅
→ (∪ 𝑤 ∈ (𝐴 ∪ {∅}) ↔ ∅ ∈
(𝐴 ∪
{∅}))) |
20 | 19 | imbi2d 329 |
. . . . . . . . 9
⊢ ((𝑤 ∖ {∅}) = ∅
→ ((∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪ {∅}))
↔ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∅
∈ (𝐴 ∪
{∅})))) |
21 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
22 | | difexg 4735 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ V → (𝑤 ∖ {∅}) ∈
V) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∖ {∅}) ∈
V |
24 | | sseq1 3589 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → (𝑧 ⊆ 𝐴 ↔ (𝑤 ∖ {∅}) ⊆ 𝐴)) |
25 | | neeq1 2844 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → (𝑧 ≠ ∅ ↔ (𝑤 ∖ {∅}) ≠
∅)) |
26 | | soeq2 4979 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → (
[⊊] Or 𝑧
↔ [⊊] Or (𝑤 ∖ {∅}))) |
27 | 24, 25, 26 | 3anbi123d 1391 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑤 ∖ {∅}) → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) ↔ ((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})))) |
28 | | unieq 4380 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → ∪ 𝑧 =
∪ (𝑤 ∖ {∅})) |
29 | 28 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑤 ∖ {∅}) → (∪ 𝑧
∈ 𝐴 ↔ ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
30 | 27, 29 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑤 ∖ {∅}) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) ↔ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})) → ∪ (𝑤 ∖ {∅}) ∈ 𝐴))) |
31 | 23, 30 | spcv 3272 |
. . . . . . . . . . . . 13
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})) → ∪ (𝑤 ∖ {∅}) ∈ 𝐴)) |
32 | 31 | com12 32 |
. . . . . . . . . . . 12
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
33 | 32 | 3expa 1257 |
. . . . . . . . . . 11
⊢ ((((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅) ∧
[⊊] Or (𝑤
∖ {∅})) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
34 | 33 | an32s 842 |
. . . . . . . . . 10
⊢ ((((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
∧ (𝑤 ∖ {∅})
≠ ∅) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
35 | | unidif0 4764 |
. . . . . . . . . . . 12
⊢ ∪ (𝑤
∖ {∅}) = ∪ 𝑤 |
36 | 35 | eleq1i 2679 |
. . . . . . . . . . 11
⊢ (∪ (𝑤
∖ {∅}) ∈ 𝐴
↔ ∪ 𝑤 ∈ 𝐴) |
37 | | elun1 3742 |
. . . . . . . . . . 11
⊢ (∪ 𝑤
∈ 𝐴 → ∪ 𝑤
∈ (𝐴 ∪
{∅})) |
38 | 36, 37 | sylbi 206 |
. . . . . . . . . 10
⊢ (∪ (𝑤
∖ {∅}) ∈ 𝐴
→ ∪ 𝑤 ∈ (𝐴 ∪ {∅})) |
39 | 34, 38 | syl6 34 |
. . . . . . . . 9
⊢ ((((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
∧ (𝑤 ∖ {∅})
≠ ∅) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
40 | | 0ex 4718 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
41 | 40 | snid 4155 |
. . . . . . . . . . 11
⊢ ∅
∈ {∅} |
42 | | elun2 3743 |
. . . . . . . . . . 11
⊢ (∅
∈ {∅} → ∅ ∈ (𝐴 ∪ {∅})) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . 10
⊢ ∅
∈ (𝐴 ∪
{∅}) |
44 | 43 | 2a1i 12 |
. . . . . . . . 9
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
→ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∅
∈ (𝐴 ∪
{∅}))) |
45 | 20, 39, 44 | pm2.61ne 2867 |
. . . . . . . 8
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
→ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
46 | 14, 45 | sylan2 490 |
. . . . . . 7
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or 𝑤) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
47 | 11, 46 | sylanb 488 |
. . . . . 6
⊢ ((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
48 | 47 | com12 32 |
. . . . 5
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
49 | 48 | alrimiv 1842 |
. . . 4
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) →
∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
50 | 49 | 3ad2ant3 1077 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) →
∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
51 | | zorng 9209 |
. . 3
⊢ (((𝐴 ∪ {∅}) ∈ dom
card ∧ ∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) → ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦) |
52 | 7, 50, 51 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) →
∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦) |
53 | | ssun1 3738 |
. . . . 5
⊢ 𝐴 ⊆ (𝐴 ∪ {∅}) |
54 | | ssralv 3629 |
. . . . 5
⊢ (𝐴 ⊆ (𝐴 ∪ {∅}) → (∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦 → ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |
55 | 53, 54 | ax-mp 5 |
. . . 4
⊢
(∀𝑦 ∈
(𝐴 ∪ {∅}) ¬
𝑥 ⊊ 𝑦 → ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
56 | 55 | reximi 2994 |
. . 3
⊢
(∃𝑥 ∈
(𝐴 ∪
{∅})∀𝑦 ∈
(𝐴 ∪ {∅}) ¬
𝑥 ⊊ 𝑦 → ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
57 | | rexun 3755 |
. . . 4
⊢
(∃𝑥 ∈
(𝐴 ∪
{∅})∀𝑦 ∈
𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ∨ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |
58 | | simpr 476 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
59 | | simpr 476 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
60 | | psseq1 3656 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑥 ⊊ 𝑦 ↔ ∅ ⊊ 𝑦)) |
61 | | 0pss 3965 |
. . . . . . . . . . . . 13
⊢ (∅
⊊ 𝑦 ↔ 𝑦 ≠ ∅) |
62 | 60, 61 | syl6bb 275 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑥 ⊊ 𝑦 ↔ 𝑦 ≠ ∅)) |
63 | 62 | notbid 307 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (¬ 𝑥 ⊊ 𝑦 ↔ ¬ 𝑦 ≠ ∅)) |
64 | | nne 2786 |
. . . . . . . . . . 11
⊢ (¬
𝑦 ≠ ∅ ↔ 𝑦 = ∅) |
65 | 63, 64 | syl6bb 275 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (¬ 𝑥 ⊊ 𝑦 ↔ 𝑦 = ∅)) |
66 | 65 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑦 = ∅)) |
67 | 40, 66 | rexsn 4170 |
. . . . . . . 8
⊢
(∃𝑥 ∈
{∅}∀𝑦 ∈
𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑦 = ∅) |
68 | | eqsn 4301 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ → (𝐴 = {∅} ↔
∀𝑦 ∈ 𝐴 𝑦 = ∅)) |
69 | 68 | biimpar 501 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑦 = ∅) → 𝐴 = {∅}) |
70 | 67, 69 | sylan2b 491 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → 𝐴 = {∅}) |
71 | 70 | rexeqdv 3122 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |
72 | 59, 71 | mpbird 246 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
73 | 58, 72 | jaodan 822 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ∨ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
74 | 57, 73 | sylan2b 491 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
75 | 56, 74 | sylan2 490 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
76 | 1, 52, 75 | syl2anc 691 |
1
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |