| Step | Hyp | Ref
| Expression |
| 1 | | noinfbnd1.1 |
. . . . . 6
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) |
| 2 | 1 | noinfno 27763 |
. . . . 5
⊢ ((𝐵 ⊆
No ∧ 𝐵 ∈
𝑉) → 𝑇 ∈ No
) |
| 3 | 2 | 3ad2ant2 1135 |
. . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑇 ∈ No
) |
| 4 | | nodmord 27698 |
. . . 4
⊢ (𝑇 ∈
No → Ord dom 𝑇) |
| 5 | | ordirr 6402 |
. . . 4
⊢ (Ord dom
𝑇 → ¬ dom 𝑇 ∈ dom 𝑇) |
| 6 | 3, 4, 5 | 3syl 18 |
. . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ dom 𝑇 ∈ dom 𝑇) |
| 7 | | simpl3l 1229 |
. . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → 𝑈 ∈ 𝐵) |
| 8 | | ndmfv 6941 |
. . . . . . . 8
⊢ (¬
dom 𝑇 ∈ dom 𝑈 → (𝑈‘dom 𝑇) = ∅) |
| 9 | | 1n0 8526 |
. . . . . . . . . . 11
⊢
1o ≠ ∅ |
| 10 | 9 | necomi 2995 |
. . . . . . . . . 10
⊢ ∅
≠ 1o |
| 11 | | neeq1 3003 |
. . . . . . . . . 10
⊢ ((𝑈‘dom 𝑇) = ∅ → ((𝑈‘dom 𝑇) ≠ 1o ↔ ∅ ≠
1o)) |
| 12 | 10, 11 | mpbiri 258 |
. . . . . . . . 9
⊢ ((𝑈‘dom 𝑇) = ∅ → (𝑈‘dom 𝑇) ≠ 1o) |
| 13 | 12 | neneqd 2945 |
. . . . . . . 8
⊢ ((𝑈‘dom 𝑇) = ∅ → ¬ (𝑈‘dom 𝑇) = 1o) |
| 14 | 8, 13 | syl 17 |
. . . . . . 7
⊢ (¬
dom 𝑇 ∈ dom 𝑈 → ¬ (𝑈‘dom 𝑇) = 1o) |
| 15 | 14 | con4i 114 |
. . . . . 6
⊢ ((𝑈‘dom 𝑇) = 1o → dom 𝑇 ∈ dom 𝑈) |
| 16 | 15 | adantl 481 |
. . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → dom 𝑇 ∈ dom 𝑈) |
| 17 | | simpl2l 1227 |
. . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → 𝐵 ⊆ No
) |
| 18 | 17, 7 | sseldd 3984 |
. . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → 𝑈 ∈ No
) |
| 19 | 18 | adantr 480 |
. . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → 𝑈 ∈ No
) |
| 20 | 17 | adantr 480 |
. . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → 𝐵 ⊆ No
) |
| 21 | | simprl 771 |
. . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → 𝑞 ∈ 𝐵) |
| 22 | 20, 21 | sseldd 3984 |
. . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → 𝑞 ∈ No
) |
| 23 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → 𝑇 ∈ No
) |
| 24 | | nodmon 27695 |
. . . . . . . . . 10
⊢ (𝑇 ∈
No → dom 𝑇
∈ On) |
| 25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → dom 𝑇 ∈ On) |
| 26 | 25 | adantr 480 |
. . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → dom 𝑇 ∈ On) |
| 27 | | simpl3r 1230 |
. . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → (𝑈 ↾ dom 𝑇) = 𝑇) |
| 28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝑈 ↾ dom 𝑇) = 𝑇) |
| 29 | | simpll1 1213 |
. . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) |
| 30 | | simpll2 1214 |
. . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉)) |
| 31 | | simpll3 1215 |
. . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) |
| 32 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) |
| 33 | 1 | noinfbnd1lem2 27769 |
. . . . . . . . . 10
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ ((𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞))) → (𝑞 ↾ dom 𝑇) = 𝑇) |
| 34 | 29, 30, 31, 32, 33 | syl112anc 1376 |
. . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝑞 ↾ dom 𝑇) = 𝑇) |
| 35 | 28, 34 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝑈 ↾ dom 𝑇) = (𝑞 ↾ dom 𝑇)) |
| 36 | | simplr 769 |
. . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝑈‘dom 𝑇) = 1o) |
| 37 | | simprr 773 |
. . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → ¬ 𝑈 <s 𝑞) |
| 38 | | nogesgn1ores 27719 |
. . . . . . . 8
⊢ (((𝑈 ∈
No ∧ 𝑞 ∈
No ∧ dom 𝑇 ∈ On) ∧ ((𝑈 ↾ dom 𝑇) = (𝑞 ↾ dom 𝑇) ∧ (𝑈‘dom 𝑇) = 1o) ∧ ¬ 𝑈 <s 𝑞) → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)) |
| 39 | 19, 22, 26, 35, 36, 37, 38 | syl321anc 1394 |
. . . . . . 7
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ (𝑞 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑞)) → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)) |
| 40 | 39 | expr 456 |
. . . . . 6
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) ∧ 𝑞 ∈ 𝐵) → (¬ 𝑈 <s 𝑞 → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))) |
| 41 | 40 | ralrimiva 3146 |
. . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → ∀𝑞 ∈ 𝐵 (¬ 𝑈 <s 𝑞 → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))) |
| 42 | | dmeq 5914 |
. . . . . . . 8
⊢ (𝑝 = 𝑈 → dom 𝑝 = dom 𝑈) |
| 43 | 42 | eleq2d 2827 |
. . . . . . 7
⊢ (𝑝 = 𝑈 → (dom 𝑇 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑈)) |
| 44 | | breq1 5146 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑈 → (𝑝 <s 𝑞 ↔ 𝑈 <s 𝑞)) |
| 45 | 44 | notbid 318 |
. . . . . . . . 9
⊢ (𝑝 = 𝑈 → (¬ 𝑝 <s 𝑞 ↔ ¬ 𝑈 <s 𝑞)) |
| 46 | | reseq1 5991 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑈 → (𝑝 ↾ suc dom 𝑇) = (𝑈 ↾ suc dom 𝑇)) |
| 47 | 46 | eqeq1d 2739 |
. . . . . . . . 9
⊢ (𝑝 = 𝑈 → ((𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇) ↔ (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))) |
| 48 | 45, 47 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑝 = 𝑈 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)) ↔ (¬ 𝑈 <s 𝑞 → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)))) |
| 49 | 48 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑝 = 𝑈 → (∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)) ↔ ∀𝑞 ∈ 𝐵 (¬ 𝑈 <s 𝑞 → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)))) |
| 50 | 43, 49 | anbi12d 632 |
. . . . . 6
⊢ (𝑝 = 𝑈 → ((dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))) ↔ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑈 <s 𝑞 → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))))) |
| 51 | 50 | rspcev 3622 |
. . . . 5
⊢ ((𝑈 ∈ 𝐵 ∧ (dom 𝑇 ∈ dom 𝑈 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑈 <s 𝑞 → (𝑈 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)))) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)))) |
| 52 | 7, 16, 41, 51 | syl12anc 837 |
. . . 4
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)))) |
| 53 | 1 | noinfdm 27764 |
. . . . . . . 8
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))}) |
| 54 | 53 | eleq2d 2827 |
. . . . . . 7
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → (dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})) |
| 55 | 54 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (dom 𝑇 ∈ dom 𝑇 ↔ dom 𝑇 ∈ {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))})) |
| 56 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑧 = dom 𝑇 → (𝑧 ∈ dom 𝑝 ↔ dom 𝑇 ∈ dom 𝑝)) |
| 57 | | suceq 6450 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = dom 𝑇 → suc 𝑧 = suc dom 𝑇) |
| 58 | 57 | reseq2d 5997 |
. . . . . . . . . . . . 13
⊢ (𝑧 = dom 𝑇 → (𝑝 ↾ suc 𝑧) = (𝑝 ↾ suc dom 𝑇)) |
| 59 | 57 | reseq2d 5997 |
. . . . . . . . . . . . 13
⊢ (𝑧 = dom 𝑇 → (𝑞 ↾ suc 𝑧) = (𝑞 ↾ suc dom 𝑇)) |
| 60 | 58, 59 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑧 = dom 𝑇 → ((𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧) ↔ (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))) |
| 61 | 60 | imbi2d 340 |
. . . . . . . . . . 11
⊢ (𝑧 = dom 𝑇 → ((¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)) ↔ (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)))) |
| 62 | 61 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (𝑧 = dom 𝑇 → (∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)) ↔ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇)))) |
| 63 | 56, 62 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑧 = dom 𝑇 → ((𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) ↔ (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))))) |
| 64 | 63 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑧 = dom 𝑇 → (∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧))) ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))))) |
| 65 | 64 | elabg 3676 |
. . . . . . 7
⊢ (dom
𝑇 ∈ On → (dom
𝑇 ∈ {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))))) |
| 66 | 3, 24, 65 | 3syl 18 |
. . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (dom 𝑇 ∈ {𝑧 ∣ ∃𝑝 ∈ 𝐵 (𝑧 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc 𝑧) = (𝑞 ↾ suc 𝑧)))} ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))))) |
| 67 | 55, 66 | bitrd 279 |
. . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (dom 𝑇 ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))))) |
| 68 | 67 | adantr 480 |
. . . 4
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → (dom 𝑇 ∈ dom 𝑇 ↔ ∃𝑝 ∈ 𝐵 (dom 𝑇 ∈ dom 𝑝 ∧ ∀𝑞 ∈ 𝐵 (¬ 𝑝 <s 𝑞 → (𝑝 ↾ suc dom 𝑇) = (𝑞 ↾ suc dom 𝑇))))) |
| 69 | 52, 68 | mpbird 257 |
. . 3
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = 1o) → dom 𝑇 ∈ dom 𝑇) |
| 70 | 6, 69 | mtand 816 |
. 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ (𝑈‘dom 𝑇) = 1o) |
| 71 | 70 | neqned 2947 |
1
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆ No
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ 1o) |