Proof of Theorem nosupbday
Step | Hyp | Ref
| Expression |
1 | | nosupbday.1 |
. . . 4
⊢ 𝑆 = if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
2 | 1 | nosupno 32764 |
. . 3
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → 𝑆 ∈ No ) |
3 | | bdayval 32716 |
. . 3
⊢ (𝑆 ∈
No → ( bday ‘𝑆) = dom 𝑆) |
4 | 2, 3 | syl 17 |
. 2
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → ( bday ‘𝑆) = dom 𝑆) |
5 | | iftrue 4359 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) |
6 | 1, 5 | syl5eq 2828 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) |
7 | 6 | dmeqd 5628 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉})) |
8 | | 2on 7920 |
. . . . . . . . . 10
⊢
2o ∈ On |
9 | 8 | elexi 3436 |
. . . . . . . . 9
⊢
2o ∈ V |
10 | 9 | dmsnop 5917 |
. . . . . . . 8
⊢ dom
{〈dom (℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉} = {dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)} |
11 | 10 | uneq2i 4027 |
. . . . . . 7
⊢ (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) = (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)}) |
12 | | dmun 5633 |
. . . . . . 7
⊢ dom
((℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) = (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ dom {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) |
13 | | df-suc 6040 |
. . . . . . 7
⊢ suc dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) = (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)}) |
14 | 11, 12, 13 | 3eqtr4i 2814 |
. . . . . 6
⊢ dom
((℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}) = suc dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) |
15 | 7, 14 | syl6eq 2832 |
. . . . 5
⊢
(∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) |
16 | 15 | adantr 473 |
. . . 4
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
dom 𝑆 = suc dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) |
17 | | simprl 759 |
. . . . . . . . 9
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
𝐴 ⊆ No ) |
18 | | simpl 475 |
. . . . . . . . . . 11
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) |
19 | | nomaxmo 32762 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆
No → ∃*𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) |
20 | 19 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → ∃*𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) |
21 | 20 | adantl 474 |
. . . . . . . . . . 11
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) |
22 | | reu5 3372 |
. . . . . . . . . . 11
⊢
(∃!𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) |
23 | 18, 21, 22 | sylanbrc 575 |
. . . . . . . . . 10
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) |
24 | | riotacl 6957 |
. . . . . . . . . 10
⊢
(∃!𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) |
26 | 17, 25 | sseldd 3861 |
. . . . . . . 8
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No
) |
27 | | bdayval 32716 |
. . . . . . . 8
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No
→ ( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) = dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) = dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) |
29 | | bdayfo 32743 |
. . . . . . . . 9
⊢ bday : No –onto→On |
30 | | fofn 6426 |
. . . . . . . . 9
⊢ ( bday : No –onto→On → bday
Fn No ) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . 8
⊢ bday Fn No
|
32 | | fnfvima 6826 |
. . . . . . . 8
⊢ (( bday Fn No ∧ 𝐴 ⊆
No ∧ (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ 𝐴) → ( bday
‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday
“ 𝐴)) |
33 | 31, 17, 25, 32 | mp3an2i 1446 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
( bday ‘(℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) ∈ ( bday
“ 𝐴)) |
34 | 28, 33 | eqeltrrd 2869 |
. . . . . 6
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
dom (℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ ( bday
“ 𝐴)) |
35 | | elssuni 4746 |
. . . . . 6
⊢ (dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ ( bday
“ 𝐴) → dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ ∪ ( bday “ 𝐴)) |
36 | 34, 35 | syl 17 |
. . . . 5
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
dom (℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ ∪ ( bday “ 𝐴)) |
37 | | nodmord 32721 |
. . . . . . 7
⊢
((℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∈ No
→ Ord dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) |
38 | 26, 37 | syl 17 |
. . . . . 6
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
Ord dom (℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦)) |
39 | | imassrn 5786 |
. . . . . . . 8
⊢ ( bday “ 𝐴) ⊆ ran bday
|
40 | | forn 6427 |
. . . . . . . . 9
⊢ ( bday : No –onto→On → ran
bday = On) |
41 | 29, 40 | ax-mp 5 |
. . . . . . . 8
⊢ ran bday = On |
42 | 39, 41 | sseqtri 3895 |
. . . . . . 7
⊢ ( bday “ 𝐴) ⊆ On |
43 | | ssorduni 7322 |
. . . . . . 7
⊢ (( bday “ 𝐴) ⊆ On → Ord ∪ ( bday “ 𝐴)) |
44 | 42, 43 | ax-mp 5 |
. . . . . 6
⊢ Ord ∪ ( bday “ 𝐴) |
45 | | ordsucsssuc 7360 |
. . . . . 6
⊢ ((Ord dom
(℩𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∧ Ord ∪
( bday “ 𝐴)) → (dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ ∪ ( bday “ 𝐴) ↔ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ∪
( bday “ 𝐴))) |
46 | 38, 44, 45 | sylancl 578 |
. . . . 5
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
(dom (℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ ∪ ( bday “ 𝐴) ↔ suc dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ∪
( bday “ 𝐴))) |
47 | 36, 46 | mpbid 224 |
. . . 4
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
suc dom (℩𝑥
∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ⊆ suc ∪
( bday “ 𝐴)) |
48 | 16, 47 | eqsstrd 3897 |
. . 3
⊢
((∃𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
dom 𝑆 ⊆ suc ∪ ( bday “ 𝐴)) |
49 | | iffalse 4362 |
. . . . . . . 8
⊢ (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if(∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦, ((℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦) ∪ {〈dom (℩𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦), 2o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
50 | 1, 49 | syl5eq 2828 |
. . . . . . 7
⊢ (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
51 | 50 | dmeqd 5628 |
. . . . . 6
⊢ (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
52 | | iotaex 6174 |
. . . . . . 7
⊢
(℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)) ∈ V |
53 | | eqid 2780 |
. . . . . . 7
⊢ (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) |
54 | 52, 53 | dmmpti 6327 |
. . . . . 6
⊢ dom
(𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐴 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥))) = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} |
55 | 51, 54 | syl6eq 2832 |
. . . . 5
⊢ (¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) |
56 | 55 | adantr 473 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
dom 𝑆 = {𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))}) |
57 | | ssel2 3855 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ⊆
No ∧ 𝑢 ∈
𝐴) → 𝑢 ∈
No ) |
58 | | bdayval 32716 |
. . . . . . . . . . . . . 14
⊢ (𝑢 ∈
No → ( bday ‘𝑢) = dom 𝑢) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆
No ∧ 𝑢 ∈
𝐴) → ( bday ‘𝑢) = dom 𝑢) |
60 | | fnfvima 6826 |
. . . . . . . . . . . . . 14
⊢ (( bday Fn No ∧ 𝐴 ⊆
No ∧ 𝑢 ∈
𝐴) → ( bday ‘𝑢) ∈ ( bday
“ 𝐴)) |
61 | 31, 60 | mp3an1 1428 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆
No ∧ 𝑢 ∈
𝐴) → ( bday ‘𝑢) ∈ ( bday
“ 𝐴)) |
62 | 59, 61 | eqeltrrd 2869 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆
No ∧ 𝑢 ∈
𝐴) → dom 𝑢 ∈ (
bday “ 𝐴)) |
63 | 62 | adantlr 703 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ∈ ( bday
“ 𝐴)) |
64 | | elssuni 4746 |
. . . . . . . . . . 11
⊢ (dom
𝑢 ∈ ( bday “ 𝐴) → dom 𝑢 ⊆ ∪ ( bday “ 𝐴)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ⊆ ∪ ( bday “ 𝐴)) |
66 | | sssucid 6111 |
. . . . . . . . . 10
⊢ ∪ ( bday “ 𝐴) ⊆ suc ∪ ( bday “ 𝐴) |
67 | 65, 66 | syl6ss 3872 |
. . . . . . . . 9
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ 𝑢 ∈ 𝐴) → dom 𝑢 ⊆ suc ∪
( bday “ 𝐴)) |
68 | 67 | sseld 3859 |
. . . . . . . 8
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ 𝑢 ∈ 𝐴) → (𝑦 ∈ dom 𝑢 → 𝑦 ∈ suc ∪
( bday “ 𝐴))) |
69 | 68 | adantrd 484 |
. . . . . . 7
⊢ (((𝐴 ⊆
No ∧ 𝐴 ∈
V) ∧ 𝑢 ∈ 𝐴) → ((𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ suc ∪
( bday “ 𝐴))) |
70 | 69 | rexlimdva 3231 |
. . . . . 6
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → (∃𝑢 ∈
𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦))) → 𝑦 ∈ suc ∪
( bday “ 𝐴))) |
71 | 70 | abssdv 3937 |
. . . . 5
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → {𝑦 ∣
∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ suc ∪
( bday “ 𝐴)) |
72 | 71 | adantl 474 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
{𝑦 ∣ ∃𝑢 ∈ 𝐴 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ⊆ suc ∪
( bday “ 𝐴)) |
73 | 56, 72 | eqsstrd 3897 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ (𝐴 ⊆ No
∧ 𝐴 ∈ V)) →
dom 𝑆 ⊆ suc ∪ ( bday “ 𝐴)) |
74 | 48, 73 | pm2.61ian 800 |
. 2
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → dom 𝑆 ⊆ suc
∪ ( bday “ 𝐴)) |
75 | 4, 74 | eqsstrd 3897 |
1
⊢ ((𝐴 ⊆
No ∧ 𝐴 ∈
V) → ( bday ‘𝑆) ⊆ suc ∪
( bday “ 𝐴)) |