| Step | Hyp | Ref
| Expression |
| 1 | | noinfbday.1 |
. . . . 5
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 2 | 1 | noinfno 27763 |
. . . 4
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) → 𝑇 ∈ No
) |
| 3 | | bdayval 27693 |
. . . 4
⊢ (𝑇 ∈
No → ( bday ‘𝑇) = dom 𝑇) |
| 4 | 2, 3 | syl 17 |
. . 3
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) → ( bday ‘𝑇) = dom 𝑇) |
| 5 | 4 | adantr 480 |
. 2
⊢ (((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) → ( bday ‘𝑇) = dom 𝑇) |
| 6 | | iftrue 4531 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) = ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉})) |
| 7 | 1, 6 | eqtrid 2789 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → 𝑇 = ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉})) |
| 8 | 7 | dmeqd 5916 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = dom ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉})) |
| 9 | | 1oex 8516 |
. . . . . . . . 9
⊢
1o ∈ V |
| 10 | 9 | dmsnop 6236 |
. . . . . . . 8
⊢ dom
{〈dom (℩𝑥
∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉} = {dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)} |
| 11 | 10 | uneq2i 4165 |
. . . . . . 7
⊢ (dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}) = (dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)}) |
| 12 | | dmun 5921 |
. . . . . . 7
⊢ dom
((℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}) = (dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ dom {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}) |
| 13 | | df-suc 6390 |
. . . . . . 7
⊢ suc dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) = (dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)}) |
| 14 | 11, 12, 13 | 3eqtr4i 2775 |
. . . . . 6
⊢ dom
((℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}) = suc dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) |
| 15 | 8, 14 | eqtrdi 2793 |
. . . . 5
⊢
(∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) |
| 16 | 15 | adantr 480 |
. . . 4
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → dom
𝑇 = suc dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) |
| 17 | | simprrl 781 |
. . . . . 6
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → 𝑂 ∈ On) |
| 18 | | eloni 6394 |
. . . . . 6
⊢ (𝑂 ∈ On → Ord 𝑂) |
| 19 | 17, 18 | syl 17 |
. . . . 5
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → Ord
𝑂) |
| 20 | | simprll 779 |
. . . . . . . 8
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → 𝐵 ⊆
No ) |
| 21 | | simpl 482 |
. . . . . . . . . 10
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) →
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) |
| 22 | | nominmo 27744 |
. . . . . . . . . . 11
⊢ (𝐵 ⊆
No → ∃*𝑥
∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) |
| 23 | 20, 22 | syl 17 |
. . . . . . . . . 10
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) →
∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) |
| 24 | | reu5 3382 |
. . . . . . . . . 10
⊢
(∃!𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ (∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ∃*𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) |
| 25 | 21, 23, 24 | sylanbrc 583 |
. . . . . . . . 9
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) →
∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) |
| 26 | | riotacl 7405 |
. . . . . . . . 9
⊢
(∃!𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵) |
| 27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) →
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵) |
| 28 | 20, 27 | sseldd 3984 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) →
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ No
) |
| 29 | | bdayval 27693 |
. . . . . . 7
⊢
((℩𝑥
∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ No
→ ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) = dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) |
| 30 | 28, 29 | syl 17 |
. . . . . 6
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) = dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) |
| 31 | | simprrr 782 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → ( bday “ 𝐵) ⊆ 𝑂) |
| 32 | | bdayfo 27722 |
. . . . . . . . 9
⊢ bday : No –onto→On |
| 33 | | fofn 6822 |
. . . . . . . . 9
⊢ ( bday : No –onto→On → bday
Fn No ) |
| 34 | 32, 33 | ax-mp 5 |
. . . . . . . 8
⊢ bday Fn No
|
| 35 | | fnfvima 7253 |
. . . . . . . 8
⊢ (( bday Fn No ∧ 𝐵 ⊆
No ∧ (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝐵) → ( bday
‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday
“ 𝐵)) |
| 36 | 34, 20, 27, 35 | mp3an2i 1468 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) ∈ ( bday
“ 𝐵)) |
| 37 | 31, 36 | sseldd 3984 |
. . . . . 6
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → ( bday ‘(℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥)) ∈ 𝑂) |
| 38 | 30, 37 | eqeltrrd 2842 |
. . . . 5
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂) |
| 39 | | ordsucss 7838 |
. . . . 5
⊢ (Ord
𝑂 → (dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∈ 𝑂 → suc dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂)) |
| 40 | 19, 38, 39 | sylc 65 |
. . . 4
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → suc dom
(℩𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ⊆ 𝑂) |
| 41 | 16, 40 | eqsstrd 4018 |
. . 3
⊢
((∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → dom
𝑇 ⊆ 𝑂) |
| 42 | 1 | noinfdm 27764 |
. . . . 5
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}) |
| 43 | 42 | adantr 480 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → dom
𝑇 = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}) |
| 44 | | simplrl 777 |
. . . . . . . . . . 11
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → 𝑂 ∈ On) |
| 45 | 44, 18 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → Ord 𝑂) |
| 46 | | ssel2 3978 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ⊆
No ∧ 𝑝 ∈
𝐵) → 𝑝 ∈
No ) |
| 47 | 46 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → 𝑝 ∈ No
) |
| 48 | | bdayval 27693 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
No → ( bday ‘𝑝) = dom 𝑝) |
| 49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday
‘𝑝) = dom
𝑝) |
| 50 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday
“ 𝐵) ⊆
𝑂) |
| 51 | | fnfvima 7253 |
. . . . . . . . . . . . . 14
⊢ (( bday Fn No ∧ 𝐵 ⊆
No ∧ 𝑝 ∈
𝐵) → ( bday ‘𝑝) ∈ ( bday
“ 𝐵)) |
| 52 | 34, 51 | mp3an1 1450 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ⊆
No ∧ 𝑝 ∈
𝐵) → ( bday ‘𝑝) ∈ ( bday
“ 𝐵)) |
| 53 | 52 | ad4ant14 752 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday
‘𝑝) ∈
( bday “ 𝐵)) |
| 54 | 50, 53 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ( bday
‘𝑝) ∈
𝑂) |
| 55 | 49, 54 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → dom 𝑝 ∈ 𝑂) |
| 56 | | ordelss 6400 |
. . . . . . . . . 10
⊢ ((Ord
𝑂 ∧ dom 𝑝 ∈ 𝑂) → dom 𝑝 ⊆ 𝑂) |
| 57 | 45, 55, 56 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → dom 𝑝 ⊆ 𝑂) |
| 58 | 57 | sseld 3982 |
. . . . . . . 8
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → (𝑧 ∈ dom 𝑝 → 𝑧 ∈ 𝑂)) |
| 59 | 58 | adantrd 491 |
. . . . . . 7
⊢ ((((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) ∧ 𝑝 ∈ 𝐵) → ((𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧 ∈ 𝑂)) |
| 60 | 59 | rexlimdva 3155 |
. . . . . 6
⊢ (((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) →
(∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) → 𝑧 ∈ 𝑂)) |
| 61 | 60 | abssdv 4068 |
. . . . 5
⊢ (((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) → {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂) |
| 62 | 61 | adantl 481 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ⊆ 𝑂) |
| 63 | 43, 62 | eqsstrd 4018 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ((𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂))) → dom
𝑇 ⊆ 𝑂) |
| 64 | 41, 63 | pm2.61ian 812 |
. 2
⊢ (((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) → dom
𝑇 ⊆ 𝑂) |
| 65 | 5, 64 | eqsstrd 4018 |
1
⊢ (((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) ∧ (𝑂 ∈ On ∧ (
bday “ 𝐵)
⊆ 𝑂)) → ( bday ‘𝑇) ⊆ 𝑂) |