Step | Hyp | Ref
| Expression |
1 | | simp2 1062 |
. 2
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) → 𝐴 ≠ ∅) |
2 | | simp1 1061 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) → 𝐴 ∈ dom
card) |
3 | | snfi 8038 |
. . . . 5
⊢ {∅}
∈ Fin |
4 | | finnum 8774 |
. . . . 5
⊢
({∅} ∈ Fin → {∅} ∈ dom card) |
5 | 3, 4 | ax-mp 5 |
. . . 4
⊢ {∅}
∈ dom card |
6 | | unnum 9022 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ {∅}
∈ dom card) → (𝐴
∪ {∅}) ∈ dom card) |
7 | 2, 5, 6 | sylancl 694 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) → (𝐴 ∪ {∅}) ∈ dom
card) |
8 | | uncom 3757 |
. . . . . . . . 9
⊢ (𝐴 ∪ {∅}) = ({∅}
∪ 𝐴) |
9 | 8 | sseq2i 3630 |
. . . . . . . 8
⊢ (𝑤 ⊆ (𝐴 ∪ {∅}) ↔ 𝑤 ⊆ ({∅} ∪ 𝐴)) |
10 | | ssundif 4052 |
. . . . . . . 8
⊢ (𝑤 ⊆ ({∅} ∪ 𝐴) ↔ (𝑤 ∖ {∅}) ⊆ 𝐴) |
11 | 9, 10 | bitri 264 |
. . . . . . 7
⊢ (𝑤 ⊆ (𝐴 ∪ {∅}) ↔ (𝑤 ∖ {∅}) ⊆ 𝐴) |
12 | | difss 3737 |
. . . . . . . . 9
⊢ (𝑤 ∖ {∅}) ⊆
𝑤 |
13 | | soss 5053 |
. . . . . . . . 9
⊢ ((𝑤 ∖ {∅}) ⊆
𝑤 → (
[⊊] Or 𝑤
→ [⊊] Or (𝑤 ∖ {∅}))) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . 8
⊢ (
[⊊] Or 𝑤
→ [⊊] Or (𝑤 ∖ {∅})) |
15 | | ssdif0 3942 |
. . . . . . . . . . 11
⊢ (𝑤 ⊆ {∅} ↔ (𝑤 ∖ {∅}) =
∅) |
16 | | uni0b 4463 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑤 =
∅ ↔ 𝑤 ⊆
{∅}) |
17 | 16 | biimpri 218 |
. . . . . . . . . . . 12
⊢ (𝑤 ⊆ {∅} → ∪ 𝑤 =
∅) |
18 | 17 | eleq1d 2686 |
. . . . . . . . . . 11
⊢ (𝑤 ⊆ {∅} → (∪ 𝑤
∈ (𝐴 ∪ {∅})
↔ ∅ ∈ (𝐴
∪ {∅}))) |
19 | 15, 18 | sylbir 225 |
. . . . . . . . . 10
⊢ ((𝑤 ∖ {∅}) = ∅
→ (∪ 𝑤 ∈ (𝐴 ∪ {∅}) ↔ ∅ ∈
(𝐴 ∪
{∅}))) |
20 | 19 | imbi2d 330 |
. . . . . . . . 9
⊢ ((𝑤 ∖ {∅}) = ∅
→ ((∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪ {∅}))
↔ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∅
∈ (𝐴 ∪
{∅})))) |
21 | | vex 3203 |
. . . . . . . . . . . . . . 15
⊢ 𝑤 ∈ V |
22 | | difexg 4808 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ V → (𝑤 ∖ {∅}) ∈
V) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∖ {∅}) ∈
V |
24 | | sseq1 3626 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → (𝑧 ⊆ 𝐴 ↔ (𝑤 ∖ {∅}) ⊆ 𝐴)) |
25 | | neeq1 2856 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → (𝑧 ≠ ∅ ↔ (𝑤 ∖ {∅}) ≠
∅)) |
26 | | soeq2 5055 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → (
[⊊] Or 𝑧
↔ [⊊] Or (𝑤 ∖ {∅}))) |
27 | 24, 25, 26 | 3anbi123d 1399 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑤 ∖ {∅}) → ((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) ↔ ((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})))) |
28 | | unieq 4444 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 ∖ {∅}) → ∪ 𝑧 =
∪ (𝑤 ∖ {∅})) |
29 | 28 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑤 ∖ {∅}) → (∪ 𝑧
∈ 𝐴 ↔ ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
30 | 27, 29 | imbi12d 334 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑤 ∖ {∅}) → (((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) ↔ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})) → ∪ (𝑤 ∖ {∅}) ∈ 𝐴))) |
31 | 23, 30 | spcv 3299 |
. . . . . . . . . . . . 13
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})) → ∪ (𝑤 ∖ {∅}) ∈ 𝐴)) |
32 | 31 | com12 32 |
. . . . . . . . . . . 12
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅ ∧
[⊊] Or (𝑤
∖ {∅})) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
33 | 32 | 3expa 1265 |
. . . . . . . . . . 11
⊢ ((((𝑤 ∖ {∅}) ⊆
𝐴 ∧ (𝑤 ∖ {∅}) ≠ ∅) ∧
[⊊] Or (𝑤
∖ {∅})) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
34 | 33 | an32s 846 |
. . . . . . . . . 10
⊢ ((((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
∧ (𝑤 ∖ {∅})
≠ ∅) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ (𝑤
∖ {∅}) ∈ 𝐴)) |
35 | | unidif0 4838 |
. . . . . . . . . . . 12
⊢ ∪ (𝑤
∖ {∅}) = ∪ 𝑤 |
36 | 35 | eleq1i 2692 |
. . . . . . . . . . 11
⊢ (∪ (𝑤
∖ {∅}) ∈ 𝐴
↔ ∪ 𝑤 ∈ 𝐴) |
37 | | elun1 3780 |
. . . . . . . . . . 11
⊢ (∪ 𝑤
∈ 𝐴 → ∪ 𝑤
∈ (𝐴 ∪
{∅})) |
38 | 36, 37 | sylbi 207 |
. . . . . . . . . 10
⊢ (∪ (𝑤
∖ {∅}) ∈ 𝐴
→ ∪ 𝑤 ∈ (𝐴 ∪ {∅})) |
39 | 34, 38 | syl6 35 |
. . . . . . . . 9
⊢ ((((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
∧ (𝑤 ∖ {∅})
≠ ∅) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
40 | | 0ex 4790 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
41 | 40 | snid 4208 |
. . . . . . . . . . 11
⊢ ∅
∈ {∅} |
42 | | elun2 3781 |
. . . . . . . . . . 11
⊢ (∅
∈ {∅} → ∅ ∈ (𝐴 ∪ {∅})) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . 10
⊢ ∅
∈ (𝐴 ∪
{∅}) |
44 | 43 | 2a1i 12 |
. . . . . . . . 9
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
→ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∅
∈ (𝐴 ∪
{∅}))) |
45 | 20, 39, 44 | pm2.61ne 2879 |
. . . . . . . 8
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or (𝑤 ∖ {∅}))
→ (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
46 | 14, 45 | sylan2 491 |
. . . . . . 7
⊢ (((𝑤 ∖ {∅}) ⊆
𝐴 ∧ [⊊]
Or 𝑤) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
47 | 11, 46 | sylanb 489 |
. . . . . 6
⊢ ((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → (∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
48 | 47 | com12 32 |
. . . . 5
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) → ((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
49 | 48 | alrimiv 1855 |
. . . 4
⊢
(∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴) →
∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
50 | 49 | 3ad2ant3 1084 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) →
∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) |
51 | | zorng 9326 |
. . 3
⊢ (((𝐴 ∪ {∅}) ∈ dom
card ∧ ∀𝑤((𝑤 ⊆ (𝐴 ∪ {∅}) ∧ [⊊] Or
𝑤) → ∪ 𝑤
∈ (𝐴 ∪
{∅}))) → ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦) |
52 | 7, 50, 51 | syl2anc 693 |
. 2
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) →
∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦) |
53 | | ssun1 3776 |
. . . . 5
⊢ 𝐴 ⊆ (𝐴 ∪ {∅}) |
54 | | ssralv 3666 |
. . . . 5
⊢ (𝐴 ⊆ (𝐴 ∪ {∅}) → (∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦 → ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |
55 | 53, 54 | ax-mp 5 |
. . . 4
⊢
(∀𝑦 ∈
(𝐴 ∪ {∅}) ¬
𝑥 ⊊ 𝑦 → ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
56 | 55 | reximi 3011 |
. . 3
⊢
(∃𝑥 ∈
(𝐴 ∪
{∅})∀𝑦 ∈
(𝐴 ∪ {∅}) ¬
𝑥 ⊊ 𝑦 → ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
57 | | rexun 3793 |
. . . 4
⊢
(∃𝑥 ∈
(𝐴 ∪
{∅})∀𝑦 ∈
𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ∨ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |
58 | | simpr 477 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
59 | | simpr 477 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
60 | | psseq1 3694 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (𝑥 ⊊ 𝑦 ↔ ∅ ⊊ 𝑦)) |
61 | | 0pss 4013 |
. . . . . . . . . . . . 13
⊢ (∅
⊊ 𝑦 ↔ 𝑦 ≠ ∅) |
62 | 60, 61 | syl6bb 276 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (𝑥 ⊊ 𝑦 ↔ 𝑦 ≠ ∅)) |
63 | 62 | notbid 308 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (¬ 𝑥 ⊊ 𝑦 ↔ ¬ 𝑦 ≠ ∅)) |
64 | | nne 2798 |
. . . . . . . . . . 11
⊢ (¬
𝑦 ≠ ∅ ↔ 𝑦 = ∅) |
65 | 63, 64 | syl6bb 276 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (¬ 𝑥 ⊊ 𝑦 ↔ 𝑦 = ∅)) |
66 | 65 | ralbidv 2986 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑦 = ∅)) |
67 | 40, 66 | rexsn 4223 |
. . . . . . . 8
⊢
(∃𝑥 ∈
{∅}∀𝑦 ∈
𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∀𝑦 ∈ 𝐴 𝑦 = ∅) |
68 | | eqsn 4361 |
. . . . . . . . 9
⊢ (𝐴 ≠ ∅ → (𝐴 = {∅} ↔
∀𝑦 ∈ 𝐴 𝑦 = ∅)) |
69 | 68 | biimpar 502 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑦 = ∅) → 𝐴 = {∅}) |
70 | 67, 69 | sylan2b 492 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → 𝐴 = {∅}) |
71 | 70 | rexeqdv 3145 |
. . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ↔ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) |
72 | 59, 71 | mpbird 247 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
73 | 58, 72 | jaodan 826 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦 ∨ ∃𝑥 ∈ {∅}∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦)) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
74 | 57, 73 | sylan2b 492 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
75 | 56, 74 | sylan2 491 |
. 2
⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ (𝐴 ∪ {∅})∀𝑦 ∈ (𝐴 ∪ {∅}) ¬ 𝑥 ⊊ 𝑦) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |
76 | 1, 52, 75 | syl2anc 693 |
1
⊢ ((𝐴 ∈ dom card ∧ 𝐴 ≠ ∅ ∧
∀𝑧((𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or
𝑧) → ∪ 𝑧
∈ 𝐴)) →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 ⊊ 𝑦) |