| Step | Hyp | Ref
| Expression |
| 1 | | noinfbnd1.1 |
. . . 4
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 2 | 1 | noinfno 27763 |
. . 3
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) → 𝑇 ∈ No
) |
| 3 | 2 | 3ad2ant2 1135 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑇 ∈ No
) |
| 4 | | simp2l 1200 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝐵 ⊆ No
) |
| 5 | | simp3 1139 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑈 ∈ 𝐵) |
| 6 | 4, 5 | sseldd 3984 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → 𝑈 ∈ No
) |
| 7 | | nodmon 27695 |
. . . 4
⊢ (𝑇 ∈
No → dom 𝑇
∈ On) |
| 8 | 3, 7 | syl 17 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom 𝑇 ∈ On) |
| 9 | | noreson 27705 |
. . 3
⊢ ((𝑈 ∈
No ∧ dom 𝑇
∈ On) → (𝑈
↾ dom 𝑇) ∈ No ) |
| 10 | 6, 8, 9 | syl2anc 584 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (𝑈 ↾ dom 𝑇) ∈ No
) |
| 11 | | ssidd 4007 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom 𝑇 ⊆ dom 𝑇) |
| 12 | | dmres 6030 |
. . . 4
⊢ dom
(𝑈 ↾ dom 𝑇) = (dom 𝑇 ∩ dom 𝑈) |
| 13 | | inss1 4237 |
. . . 4
⊢ (dom
𝑇 ∩ dom 𝑈) ⊆ dom 𝑇 |
| 14 | 12, 13 | eqsstri 4030 |
. . 3
⊢ dom
(𝑈 ↾ dom 𝑇) ⊆ dom 𝑇 |
| 15 | 14 | a1i 11 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇) |
| 16 | | nodmord 27698 |
. . . . . . . 8
⊢ (𝑇 ∈
No → Ord dom 𝑇) |
| 17 | 3, 16 | syl 17 |
. . . . . . 7
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → Ord dom 𝑇) |
| 18 | | ordsucss 7838 |
. . . . . . 7
⊢ (Ord dom
𝑇 → (ℎ ∈ dom 𝑇 → suc ℎ ⊆ dom 𝑇)) |
| 19 | 17, 18 | syl 17 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 → suc ℎ ⊆ dom 𝑇)) |
| 20 | 19 | imp 406 |
. . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → suc ℎ ⊆ dom 𝑇) |
| 21 | 20 | resabs1d 6026 |
. . . 4
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) = (𝑈 ↾ suc ℎ)) |
| 22 | 1 | noinfdm 27764 |
. . . . . . . . 9
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))}) |
| 23 | 22 | eleq2d 2827 |
. . . . . . . 8
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (ℎ ∈ dom 𝑇 ↔ ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))})) |
| 24 | | abid 2718 |
. . . . . . . . 9
⊢ (ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))} ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))) |
| 25 | | breq2 5147 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑣 → (𝑝 <s 𝑞 ↔ 𝑝 <s 𝑣)) |
| 26 | 25 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑣 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑝 <s 𝑣)) |
| 27 | | reseq1 5991 |
. . . . . . . . . . . . . 14
⊢ (𝑞 = 𝑣 → (𝑞 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) |
| 28 | 27 | eqeq2d 2748 |
. . . . . . . . . . . . 13
⊢ (𝑞 = 𝑣 → ((𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) |
| 29 | 26, 28 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑣 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) |
| 30 | 29 | cbvralvw 3237 |
. . . . . . . . . . 11
⊢
(∀𝑞 ∈
𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) |
| 31 | 30 | anbi2i 623 |
. . . . . . . . . 10
⊢ ((ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ))) ↔ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) |
| 32 | 31 | rexbii 3094 |
. . . . . . . . 9
⊢
(∃𝑝 ∈
𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ))) ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) |
| 33 | 24, 32 | bitri 275 |
. . . . . . . 8
⊢ (ℎ ∈ {ℎ ∣ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc ℎ) = (𝑞 ↾ suc ℎ)))} ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) |
| 34 | 23, 33 | bitrdi 287 |
. . . . . . 7
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (ℎ ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) |
| 35 | 34 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) |
| 36 | | simpl2l 1227 |
. . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝐵 ⊆ No
) |
| 37 | | simprl 771 |
. . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ 𝐵) |
| 38 | 36, 37 | sseldd 3984 |
. . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑝 ∈ No
) |
| 39 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ No
) |
| 40 | | sltso 27721 |
. . . . . . . . . . . 12
⊢ <s Or
No |
| 41 | | soasym 5625 |
. . . . . . . . . . . 12
⊢ (( <s
Or No ∧ (𝑝 ∈ No
∧ 𝑈 ∈ No )) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝)) |
| 42 | 40, 41 | mpan 690 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈
No ∧ 𝑈 ∈
No ) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝)) |
| 43 | 38, 39, 42 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝)) |
| 44 | | nodmon 27695 |
. . . . . . . . . . . . . 14
⊢ (𝑝 ∈
No → dom 𝑝
∈ On) |
| 45 | 38, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → dom 𝑝 ∈ On) |
| 46 | | simprrl 781 |
. . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ dom 𝑝) |
| 47 | | onelon 6409 |
. . . . . . . . . . . . 13
⊢ ((dom
𝑝 ∈ On ∧ ℎ ∈ dom 𝑝) → ℎ ∈ On) |
| 48 | 45, 46, 47 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ℎ ∈ On) |
| 49 | | onsucb 7837 |
. . . . . . . . . . . 12
⊢ (ℎ ∈ On ↔ suc ℎ ∈ On) |
| 50 | 48, 49 | sylib 218 |
. . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → suc ℎ ∈ On) |
| 51 | | sltres 27707 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈
No ∧ 𝑝 ∈
No ∧ suc ℎ ∈ On) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) → 𝑈 <s 𝑝)) |
| 52 | 39, 38, 50, 51 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) → 𝑈 <s 𝑝)) |
| 53 | 43, 52 | nsyld 156 |
. . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ))) |
| 54 | | noreson 27705 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈
No ∧ suc ℎ
∈ On) → (𝑈
↾ suc ℎ) ∈ No ) |
| 55 | 39, 50, 54 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑈 ↾ suc ℎ) ∈ No
) |
| 56 | | sonr 5616 |
. . . . . . . . . . . . . 14
⊢ (( <s
Or No ∧ (𝑈 ↾ suc ℎ) ∈ No )
→ ¬ (𝑈 ↾ suc
ℎ) <s (𝑈 ↾ suc ℎ)) |
| 57 | 40, 56 | mpan 690 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ↾ suc ℎ) ∈ No
→ ¬ (𝑈 ↾ suc
ℎ) <s (𝑈 ↾ suc ℎ)) |
| 58 | 55, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ)) |
| 60 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑈 → (𝑝 <s 𝑣 ↔ 𝑝 <s 𝑈)) |
| 61 | 60 | notbid 318 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑈 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑈)) |
| 62 | | reseq1 5991 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 = 𝑈 → (𝑣 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)) |
| 63 | 62 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 = 𝑈 → ((𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ) ↔ (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))) |
| 64 | 61, 63 | imbi12d 344 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑈 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)) ↔ (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)))) |
| 65 | | simprrr 782 |
. . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) |
| 66 | | simpl3 1194 |
. . . . . . . . . . . . . 14
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → 𝑈 ∈ 𝐵) |
| 67 | 64, 65, 66 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑝 <s 𝑈 → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ))) |
| 68 | 67 | imp 406 |
. . . . . . . . . . . 12
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → (𝑝 ↾ suc ℎ) = (𝑈 ↾ suc ℎ)) |
| 69 | 68 | breq2d 5155 |
. . . . . . . . . . 11
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → ((𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ) ↔ (𝑈 ↾ suc ℎ) <s (𝑈 ↾ suc ℎ))) |
| 70 | 59, 69 | mtbird 325 |
. . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) ∧ ¬ 𝑝 <s 𝑈) → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ)) |
| 71 | 70 | ex 412 |
. . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (¬ 𝑝 <s 𝑈 → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ))) |
| 72 | 53, 71 | pm2.61d 179 |
. . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ)) |
| 73 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) |
| 74 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉)) |
| 75 | 1 | noinfres 27767 |
. . . . . . . . . 10
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑝 ∈ 𝐵 ∧ ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ)))) → (𝑇 ↾ suc ℎ) = (𝑝 ↾ suc ℎ)) |
| 76 | 73, 74, 37, 46, 65, 75 | syl113anc 1384 |
. . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → (𝑇 ↾ suc ℎ) = (𝑝 ↾ suc ℎ)) |
| 77 | 76 | breq2d 5155 |
. . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ((𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ) ↔ (𝑈 ↾ suc ℎ) <s (𝑝 ↾ suc ℎ))) |
| 78 | 72, 77 | mtbird 325 |
. . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ)) |
| 79 | 78 | rexlimdvaa 3156 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (∃𝑝 ∈ 𝐵 (ℎ ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc ℎ) = (𝑣 ↾ suc ℎ))) → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))) |
| 80 | 35, 79 | sylbid 240 |
. . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → (ℎ ∈ dom 𝑇 → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))) |
| 81 | 80 | imp 406 |
. . . 4
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ¬ (𝑈 ↾ suc ℎ) <s (𝑇 ↾ suc ℎ)) |
| 82 | 21, 81 | eqnbrtrd 5161 |
. . 3
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) ∧ ℎ ∈ dom 𝑇) → ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ)) |
| 83 | 82 | ralrimiva 3146 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → ∀ℎ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ)) |
| 84 | | noresle 27742 |
. 2
⊢ (((𝑇 ∈
No ∧ (𝑈 ↾
dom 𝑇) ∈ No ) ∧ (dom 𝑇 ⊆ dom 𝑇 ∧ dom (𝑈 ↾ dom 𝑇) ⊆ dom 𝑇 ∧ ∀ℎ ∈ dom 𝑇 ¬ ((𝑈 ↾ dom 𝑇) ↾ suc ℎ) <s (𝑇 ↾ suc ℎ))) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇) |
| 85 | 3, 10, 11, 15, 83, 84 | syl23anc 1379 |
1
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ 𝑈 ∈ 𝐵) → ¬ (𝑈 ↾ dom 𝑇) <s 𝑇) |