Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . 3
⊢ (𝑏 ∈ ω ↦ ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) = (𝑏 ∈ ω ↦ ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
2 | 1 | rnmpt 5371 |
. 2
⊢ ran
(𝑏 ∈ ω ↦
∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) = {𝑑 ∣ ∃𝑏 ∈ ω 𝑑 = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}} |
3 | | unieq 4444 |
. . . . . . . . . . . 12
⊢ ({𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅ → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∪
∅) |
4 | | uni0 4465 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
5 | 3, 4 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ({𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅ → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅) |
6 | 5 | adantl 482 |
. . . . . . . . . 10
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅) → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅) |
7 | | 0ex 4790 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
8 | 7 | elsn2 4211 |
. . . . . . . . . 10
⊢ (∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {∅} ↔ ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅) |
9 | 6, 8 | sylibr 224 |
. . . . . . . . 9
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅) → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {∅}) |
10 | 9 | olcd 408 |
. . . . . . . 8
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∅) → (∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ 𝐴 ∨ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {∅})) |
11 | | ssrab2 3687 |
. . . . . . . . . 10
⊢ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ⊆ 𝐴 |
12 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) |
13 | | simplll 798 |
. . . . . . . . . . . 12
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → [⊊] Or
𝐴) |
14 | | simpllr 799 |
. . . . . . . . . . . 12
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → 𝐴 ⊆ Fin) |
15 | | simplr 792 |
. . . . . . . . . . . 12
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → 𝑏 ∈ ω) |
16 | | fin1a2lem9 9230 |
. . . . . . . . . . . 12
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin ∧
𝑏 ∈ ω) →
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ Fin) |
17 | 13, 14, 15, 16 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ Fin) |
18 | | soss 5053 |
. . . . . . . . . . . 12
⊢ ({𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ⊆ 𝐴 → ( [⊊] Or 𝐴 → [⊊] Or
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏})) |
19 | 11, 13, 18 | mpsyl 68 |
. . . . . . . . . . 11
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → [⊊] Or
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
20 | | fin1a2lem10 9231 |
. . . . . . . . . . 11
⊢ (({𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅ ∧ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ Fin ∧ [⊊] Or
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) → ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
21 | 12, 17, 19, 20 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
22 | 11, 21 | sseldi 3601 |
. . . . . . . . 9
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ 𝐴) |
23 | 22 | orcd 407 |
. . . . . . . 8
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) ∧
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ≠ ∅) → (∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ 𝐴 ∨ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {∅})) |
24 | 10, 23 | pm2.61dane 2881 |
. . . . . . 7
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) →
(∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ 𝐴 ∨ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {∅})) |
25 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑑 = ∪
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} → (𝑑 ∈ 𝐴 ↔ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ 𝐴)) |
26 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑑 = ∪
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} → (𝑑 ∈ {∅} ↔ ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {∅})) |
27 | 25, 26 | orbi12d 746 |
. . . . . . 7
⊢ (𝑑 = ∪
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} → ((𝑑 ∈ 𝐴 ∨ 𝑑 ∈ {∅}) ↔ (∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ 𝐴 ∨ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ∈ {∅}))) |
28 | 24, 27 | syl5ibrcom 237 |
. . . . . 6
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑏 ∈ ω) →
(𝑑 = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} → (𝑑 ∈ 𝐴 ∨ 𝑑 ∈ {∅}))) |
29 | 28 | rexlimdva 3031 |
. . . . 5
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
(∃𝑏 ∈ ω
𝑑 = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} → (𝑑 ∈ 𝐴 ∨ 𝑑 ∈ {∅}))) |
30 | | simpr 477 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
𝐴 ⊆
Fin) |
31 | 30 | sselda 3603 |
. . . . . . . . 9
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → 𝑑 ∈ Fin) |
32 | | ficardom 8787 |
. . . . . . . . 9
⊢ (𝑑 ∈ Fin →
(card‘𝑑) ∈
ω) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → (card‘𝑑) ∈ ω) |
34 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → 𝑑 ∈ 𝐴) |
35 | | ficardid 8788 |
. . . . . . . . . . . . 13
⊢ (𝑑 ∈ Fin →
(card‘𝑑) ≈
𝑑) |
36 | 31, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → (card‘𝑑) ≈ 𝑑) |
37 | | ensym 8005 |
. . . . . . . . . . . 12
⊢
((card‘𝑑)
≈ 𝑑 → 𝑑 ≈ (card‘𝑑)) |
38 | | endom 7982 |
. . . . . . . . . . . 12
⊢ (𝑑 ≈ (card‘𝑑) → 𝑑 ≼ (card‘𝑑)) |
39 | 36, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → 𝑑 ≼ (card‘𝑑)) |
40 | | breq1 4656 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑑 → (𝑐 ≼ (card‘𝑑) ↔ 𝑑 ≼ (card‘𝑑))) |
41 | 40 | elrab 3363 |
. . . . . . . . . . 11
⊢ (𝑑 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)} ↔ (𝑑 ∈ 𝐴 ∧ 𝑑 ≼ (card‘𝑑))) |
42 | 34, 39, 41 | sylanbrc 698 |
. . . . . . . . . 10
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → 𝑑 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}) |
43 | | elssuni 4467 |
. . . . . . . . . 10
⊢ (𝑑 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)} → 𝑑 ⊆ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → 𝑑 ⊆ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}) |
45 | | breq1 4656 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑏 → (𝑐 ≼ (card‘𝑑) ↔ 𝑏 ≼ (card‘𝑑))) |
46 | 45 | elrab 3363 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)} ↔ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) |
47 | | simprr 796 |
. . . . . . . . . . . . . . 15
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝑏 ≼ (card‘𝑑)) |
48 | 36 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → (card‘𝑑) ≈ 𝑑) |
49 | | domentr 8015 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ≼ (card‘𝑑) ∧ (card‘𝑑) ≈ 𝑑) → 𝑏 ≼ 𝑑) |
50 | 47, 48, 49 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝑏 ≼ 𝑑) |
51 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝐴 ⊆ Fin) |
52 | | simprl 794 |
. . . . . . . . . . . . . . . 16
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝑏 ∈ 𝐴) |
53 | 51, 52 | sseldd 3604 |
. . . . . . . . . . . . . . 15
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝑏 ∈ Fin) |
54 | 31 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝑑 ∈ Fin) |
55 | | simplll 798 |
. . . . . . . . . . . . . . . 16
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → [⊊] Or 𝐴) |
56 | | simplr 792 |
. . . . . . . . . . . . . . . 16
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝑑 ∈ 𝐴) |
57 | | sorpssi 6943 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑏 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴)) → (𝑏 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑏)) |
58 | 55, 52, 56, 57 | syl12anc 1324 |
. . . . . . . . . . . . . . 15
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → (𝑏 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑏)) |
59 | | fincssdom 9145 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ Fin ∧ 𝑑 ∈ Fin ∧ (𝑏 ⊆ 𝑑 ∨ 𝑑 ⊆ 𝑏)) → (𝑏 ≼ 𝑑 ↔ 𝑏 ⊆ 𝑑)) |
60 | 53, 54, 58, 59 | syl3anc 1326 |
. . . . . . . . . . . . . 14
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → (𝑏 ≼ 𝑑 ↔ 𝑏 ⊆ 𝑑)) |
61 | 50, 60 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑))) → 𝑏 ⊆ 𝑑) |
62 | 61 | ex 450 |
. . . . . . . . . . . 12
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → ((𝑏 ∈ 𝐴 ∧ 𝑏 ≼ (card‘𝑑)) → 𝑏 ⊆ 𝑑)) |
63 | 46, 62 | syl5bi 232 |
. . . . . . . . . . 11
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → (𝑏 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)} → 𝑏 ⊆ 𝑑)) |
64 | 63 | ralrimiv 2965 |
. . . . . . . . . 10
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → ∀𝑏 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}𝑏 ⊆ 𝑑) |
65 | | unissb 4469 |
. . . . . . . . . 10
⊢ (∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)} ⊆ 𝑑 ↔ ∀𝑏 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}𝑏 ⊆ 𝑑) |
66 | 64, 65 | sylibr 224 |
. . . . . . . . 9
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)} ⊆ 𝑑) |
67 | 44, 66 | eqssd 3620 |
. . . . . . . 8
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → 𝑑 = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}) |
68 | | breq2 4657 |
. . . . . . . . . . . 12
⊢ (𝑏 = (card‘𝑑) → (𝑐 ≼ 𝑏 ↔ 𝑐 ≼ (card‘𝑑))) |
69 | 68 | rabbidv 3189 |
. . . . . . . . . . 11
⊢ (𝑏 = (card‘𝑑) → {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}) |
70 | 69 | unieqd 4446 |
. . . . . . . . . 10
⊢ (𝑏 = (card‘𝑑) → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}) |
71 | 70 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑏 = (card‘𝑑) → (𝑑 = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ↔ 𝑑 = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)})) |
72 | 71 | rspcev 3309 |
. . . . . . . 8
⊢
(((card‘𝑑)
∈ ω ∧ 𝑑 =
∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ (card‘𝑑)}) → ∃𝑏 ∈ ω 𝑑 = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
73 | 33, 67, 72 | syl2anc 693 |
. . . . . . 7
⊢ (((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) ∧
𝑑 ∈ 𝐴) → ∃𝑏 ∈ ω 𝑑 = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
74 | 73 | ex 450 |
. . . . . 6
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
(𝑑 ∈ 𝐴 → ∃𝑏 ∈ ω 𝑑 = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏})) |
75 | | velsn 4193 |
. . . . . . 7
⊢ (𝑑 ∈ {∅} ↔ 𝑑 = ∅) |
76 | | peano1 7085 |
. . . . . . . . 9
⊢ ∅
∈ ω |
77 | | dom0 8088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ≼ ∅ ↔ 𝑏 = ∅) |
78 | 77 | biimpi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ≼ ∅ → 𝑏 = ∅) |
79 | 78 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ∅) → 𝑏 = ∅) |
80 | 79 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
((𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ∅) → 𝑏 = ∅)) |
81 | | breq1 4656 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑏 → (𝑐 ≼ ∅ ↔ 𝑏 ≼ ∅)) |
82 | 81 | elrab 3363 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅} ↔ (𝑏 ∈ 𝐴 ∧ 𝑏 ≼ ∅)) |
83 | | velsn 4193 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ {∅} ↔ 𝑏 = ∅) |
84 | 80, 82, 83 | 3imtr4g 285 |
. . . . . . . . . . . 12
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
(𝑏 ∈ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅} → 𝑏 ∈ {∅})) |
85 | 84 | ssrdv 3609 |
. . . . . . . . . . 11
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅} ⊆
{∅}) |
86 | | uni0b 4463 |
. . . . . . . . . . 11
⊢ (∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ ∅} = ∅
↔ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅} ⊆
{∅}) |
87 | 85, 86 | sylibr 224 |
. . . . . . . . . 10
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅} = ∅) |
88 | 87 | eqcomd 2628 |
. . . . . . . . 9
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
∅ = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅}) |
89 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑏 = ∅ → (𝑐 ≼ 𝑏 ↔ 𝑐 ≼ ∅)) |
90 | 89 | rabbidv 3189 |
. . . . . . . . . . . 12
⊢ (𝑏 = ∅ → {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅}) |
91 | 90 | unieqd 4446 |
. . . . . . . . . . 11
⊢ (𝑏 = ∅ → ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅}) |
92 | 91 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑏 = ∅ → (∅ =
∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ↔ ∅ = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼
∅})) |
93 | 92 | rspcev 3309 |
. . . . . . . . 9
⊢ ((∅
∈ ω ∧ ∅ = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ ∅}) → ∃𝑏 ∈ ω ∅ = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
94 | 76, 88, 93 | sylancr 695 |
. . . . . . . 8
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
∃𝑏 ∈ ω
∅ = ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) |
95 | | eqeq1 2626 |
. . . . . . . . 9
⊢ (𝑑 = ∅ → (𝑑 = ∪
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ↔ ∅ = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏})) |
96 | 95 | rexbidv 3052 |
. . . . . . . 8
⊢ (𝑑 = ∅ → (∃𝑏 ∈ ω 𝑑 = ∪
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ↔ ∃𝑏 ∈ ω ∅ = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏})) |
97 | 94, 96 | syl5ibrcom 237 |
. . . . . . 7
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
(𝑑 = ∅ →
∃𝑏 ∈ ω
𝑑 = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏})) |
98 | 75, 97 | syl5bi 232 |
. . . . . 6
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
(𝑑 ∈ {∅} →
∃𝑏 ∈ ω
𝑑 = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏})) |
99 | 74, 98 | jaod 395 |
. . . . 5
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
((𝑑 ∈ 𝐴 ∨ 𝑑 ∈ {∅}) → ∃𝑏 ∈ ω 𝑑 = ∪
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏})) |
100 | 29, 99 | impbid 202 |
. . . 4
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
(∃𝑏 ∈ ω
𝑑 = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ↔ (𝑑 ∈ 𝐴 ∨ 𝑑 ∈ {∅}))) |
101 | | elun 3753 |
. . . 4
⊢ (𝑑 ∈ (𝐴 ∪ {∅}) ↔ (𝑑 ∈ 𝐴 ∨ 𝑑 ∈ {∅})) |
102 | 100, 101 | syl6bbr 278 |
. . 3
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
(∃𝑏 ∈ ω
𝑑 = ∪ {𝑐
∈ 𝐴 ∣ 𝑐 ≼ 𝑏} ↔ 𝑑 ∈ (𝐴 ∪ {∅}))) |
103 | 102 | abbi1dv 2743 |
. 2
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
{𝑑 ∣ ∃𝑏 ∈ ω 𝑑 = ∪
{𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}} = (𝐴 ∪ {∅})) |
104 | 2, 103 | syl5eq 2668 |
1
⊢ ((
[⊊] Or 𝐴
∧ 𝐴 ⊆ Fin) →
ran (𝑏 ∈ ω
↦ ∪ {𝑐 ∈ 𝐴 ∣ 𝑐 ≼ 𝑏}) = (𝐴 ∪ {∅})) |