| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpl1 1192 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) | 
| 2 |  | simpl2 1193 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉)) | 
| 3 |  | simprl 771 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ 𝐵) | 
| 4 |  | simpl3 1194 | . . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) | 
| 5 |  | simp2l 1200 | . . . . . . . . . . . . 13
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝐵 ⊆  No
) | 
| 6 | 5 | sselda 3983 | . . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → 𝑤 ∈  No
) | 
| 7 |  | simp3l 1202 | . . . . . . . . . . . . . 14
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈 ∈ 𝐵) | 
| 8 | 5, 7 | sseldd 3984 | . . . . . . . . . . . . 13
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → 𝑈 ∈  No
) | 
| 9 | 8 | adantr 480 | . . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → 𝑈 ∈  No
) | 
| 10 |  | sltso 27721 | . . . . . . . . . . . . 13
⊢  <s Or
 No | 
| 11 |  | soasym 5625 | . . . . . . . . . . . . 13
⊢ (( <s
Or  No  ∧ (𝑤 ∈  No 
∧ 𝑈 ∈  No )) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤)) | 
| 12 | 10, 11 | mpan 690 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ 
No  ∧ 𝑈 ∈
 No ) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤)) | 
| 13 | 6, 9, 12 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤)) | 
| 14 | 13 | impr 454 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤) | 
| 15 | 3, 14 | jca 511 | . . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤)) | 
| 16 |  | noinfbnd1.1 | . . . . . . . . . 10
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) | 
| 17 | 16 | noinfbnd1lem2 27769 | . . . . . . . . 9
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ ((𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇) ∧ (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤))) → (𝑤 ↾ dom 𝑇) = 𝑇) | 
| 18 | 1, 2, 4, 15, 17 | syl112anc 1376 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇) | 
| 19 | 16 | noinfbnd1lem3 27770 | . . . . . . . 8
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑤 ∈ 𝐵 ∧ (𝑤 ↾ dom 𝑇) = 𝑇)) → (𝑤‘dom 𝑇) ≠ 1o) | 
| 20 | 1, 2, 3, 18, 19 | syl112anc 1376 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) ≠ 1o) | 
| 21 | 20 | neneqd 2945 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ (𝑤‘dom 𝑇) = 1o) | 
| 22 | 21 | expr 456 | . . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → ¬ (𝑤‘dom 𝑇) = 1o)) | 
| 23 |  | imnan 399 | . . . . 5
⊢ ((𝑤 <s 𝑈 → ¬ (𝑤‘dom 𝑇) = 1o) ↔ ¬ (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o)) | 
| 24 | 22, 23 | sylib 218 | . . . 4
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ 𝑤 ∈ 𝐵) → ¬ (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o)) | 
| 25 | 24 | nrexdv 3149 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ ∃𝑤 ∈ 𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o)) | 
| 26 |  | breq2 5147 | . . . . . . 7
⊢ (𝑥 = 𝑈 → (𝑦 <s 𝑥 ↔ 𝑦 <s 𝑈)) | 
| 27 | 26 | rexbidv 3179 | . . . . . 6
⊢ (𝑥 = 𝑈 → (∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑈)) | 
| 28 |  | simpl1 1192 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) | 
| 29 |  | dfral2 3099 | . . . . . . . 8
⊢
(∀𝑥 ∈
𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥 ∈ 𝐵 ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥) | 
| 30 |  | ralnex 3072 | . . . . . . . . 9
⊢
(∀𝑦 ∈
𝐵 ¬ 𝑦 <s 𝑥 ↔ ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥) | 
| 31 | 30 | rexbii 3094 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ↔ ∃𝑥 ∈ 𝐵 ¬ ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥) | 
| 32 | 29, 31 | xchbinxr 335 | . . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥 ↔ ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) | 
| 33 | 28, 32 | sylibr 234 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 𝑦 <s 𝑥) | 
| 34 |  | simpl3l 1229 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑈 ∈ 𝐵) | 
| 35 | 27, 33, 34 | rspcdva 3623 | . . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑦 ∈ 𝐵 𝑦 <s 𝑈) | 
| 36 |  | breq1 5146 | . . . . . 6
⊢ (𝑦 = 𝑤 → (𝑦 <s 𝑈 ↔ 𝑤 <s 𝑈)) | 
| 37 | 36 | cbvrexvw 3238 | . . . . 5
⊢
(∃𝑦 ∈
𝐵 𝑦 <s 𝑈 ↔ ∃𝑤 ∈ 𝐵 𝑤 <s 𝑈) | 
| 38 | 35, 37 | sylib 218 | . . . 4
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑤 ∈ 𝐵 𝑤 <s 𝑈) | 
| 39 |  | simpl2l 1227 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝐵 ⊆  No
) | 
| 40 | 39 | adantr 480 | . . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝐵 ⊆  No
) | 
| 41 |  | simprl 771 | . . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈ 𝐵) | 
| 42 | 40, 41 | sseldd 3984 | . . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 ∈  No
) | 
| 43 | 34 | adantr 480 | . . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑈 ∈ 𝐵) | 
| 44 | 40, 43 | sseldd 3984 | . . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑈 ∈  No
) | 
| 45 |  | simpl2 1193 | . . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉)) | 
| 46 | 16 | noinfno 27763 | . . . . . . . . . . 11
⊢ ((𝐵 ⊆ 
No  ∧ 𝐵 ∈
𝑉) → 𝑇 ∈  No
) | 
| 47 | 45, 46 | syl 17 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → 𝑇 ∈  No
) | 
| 48 | 47 | adantr 480 | . . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑇 ∈  No
) | 
| 49 |  | nodmon 27695 | . . . . . . . . 9
⊢ (𝑇 ∈ 
No  → dom 𝑇
∈ On) | 
| 50 | 48, 49 | syl 17 | . . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → dom 𝑇 ∈ On) | 
| 51 |  | simpll1 1213 | . . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) | 
| 52 |  | simpll2 1214 | . . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉)) | 
| 53 |  | simpll3 1215 | . . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) | 
| 54 |  | simprr 773 | . . . . . . . . . . . 12
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → 𝑤 <s 𝑈) | 
| 55 | 42, 44, 12 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 <s 𝑈 → ¬ 𝑈 <s 𝑤)) | 
| 56 | 54, 55 | mpd 15 | . . . . . . . . . . 11
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → ¬ 𝑈 <s 𝑤) | 
| 57 | 41, 56 | jca 511 | . . . . . . . . . 10
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ∈ 𝐵 ∧ ¬ 𝑈 <s 𝑤)) | 
| 58 | 51, 52, 53, 57, 17 | syl112anc 1376 | . . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = 𝑇) | 
| 59 |  | simpl3r 1230 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑈 ↾ dom 𝑇) = 𝑇) | 
| 60 | 59 | adantr 480 | . . . . . . . . 9
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈 ↾ dom 𝑇) = 𝑇) | 
| 61 | 58, 60 | eqtr4d 2780 | . . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇)) | 
| 62 |  | simplr 769 | . . . . . . . 8
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑈‘dom 𝑇) = ∅) | 
| 63 |  | nogt01o 27741 | . . . . . . . 8
⊢ (((𝑤 ∈ 
No  ∧ 𝑈 ∈
 No  ∧ dom 𝑇 ∈ On) ∧ ((𝑤 ↾ dom 𝑇) = (𝑈 ↾ dom 𝑇) ∧ 𝑤 <s 𝑈) ∧ (𝑈‘dom 𝑇) = ∅) → (𝑤‘dom 𝑇) = 1o) | 
| 64 | 42, 44, 50, 61, 54, 62, 63 | syl321anc 1394 | . . . . . . 7
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ (𝑤 ∈ 𝐵 ∧ 𝑤 <s 𝑈)) → (𝑤‘dom 𝑇) = 1o) | 
| 65 | 64 | expr 456 | . . . . . 6
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → (𝑤‘dom 𝑇) = 1o)) | 
| 66 | 65 | ancld 550 | . . . . 5
⊢ ((((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) ∧ 𝑤 ∈ 𝐵) → (𝑤 <s 𝑈 → (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o))) | 
| 67 | 66 | reximdva 3168 | . . . 4
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → (∃𝑤 ∈ 𝐵 𝑤 <s 𝑈 → ∃𝑤 ∈ 𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o))) | 
| 68 | 38, 67 | mpd 15 | . . 3
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) ∧ (𝑈‘dom 𝑇) = ∅) → ∃𝑤 ∈ 𝐵 (𝑤 <s 𝑈 ∧ (𝑤‘dom 𝑇) = 1o)) | 
| 69 | 25, 68 | mtand 816 | . 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → ¬ (𝑈‘dom 𝑇) = ∅) | 
| 70 | 69 | neqned 2947 | 1
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ (𝑈 ↾ dom 𝑇) = 𝑇)) → (𝑈‘dom 𝑇) ≠ ∅) |