| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dmres 6029 | . . . 4
⊢ dom
(𝑇 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑇) | 
| 2 |  | noinfres.1 | . . . . . . . . 9
⊢ 𝑇 = if(∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥, ((℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) ∪ {〈dom (℩𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥), 1o〉}), (𝑔 ∈ {𝑦 ∣ ∃𝑢 ∈ 𝐵 (𝑦 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑦) = (𝑣 ↾ suc 𝑦)))} ↦ (℩𝑥∃𝑢 ∈ 𝐵 (𝑔 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝑔) = (𝑣 ↾ suc 𝑔)) ∧ (𝑢‘𝑔) = 𝑥)))) | 
| 3 | 2 | noinfno 27764 | . . . . . . . 8
⊢ ((𝐵 ⊆ 
No  ∧ 𝐵 ∈
𝑉) → 𝑇 ∈  No
) | 
| 4 | 3 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑇 ∈  No
) | 
| 5 |  | nodmord 27699 | . . . . . . 7
⊢ (𝑇 ∈ 
No  → Ord dom 𝑇) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑇) | 
| 7 |  | simp31 1209 | . . . . . . . . 9
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈 ∈ 𝐵) | 
| 8 |  | simp32 1210 | . . . . . . . . 9
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑈) | 
| 9 |  | simp33 1211 | . . . . . . . . 9
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) | 
| 10 |  | dmeq 5913 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑈 → dom 𝑏 = dom 𝑈) | 
| 11 | 10 | eleq2d 2826 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑈 → (𝐺 ∈ dom 𝑏 ↔ 𝐺 ∈ dom 𝑈)) | 
| 12 |  | breq1 5145 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑈 → (𝑏 <s 𝑐 ↔ 𝑈 <s 𝑐)) | 
| 13 | 12 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑈 → (¬ 𝑏 <s 𝑐 ↔ ¬ 𝑈 <s 𝑐)) | 
| 14 |  | reseq1 5990 | . . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑈 → (𝑏 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺)) | 
| 15 | 14 | eqeq1d 2738 | . . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑈 → ((𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))) | 
| 16 | 13, 15 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑏 = 𝑈 → ((¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ (¬ 𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))) | 
| 17 | 16 | ralbidv 3177 | . . . . . . . . . . . 12
⊢ (𝑏 = 𝑈 → (∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ ∀𝑐 ∈ 𝐵 (¬ 𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))) | 
| 18 |  | breq2 5146 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑣 → (𝑈 <s 𝑐 ↔ 𝑈 <s 𝑣)) | 
| 19 | 18 | notbid 318 | . . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑣 → (¬ 𝑈 <s 𝑐 ↔ ¬ 𝑈 <s 𝑣)) | 
| 20 |  | reseq1 5990 | . . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑣 → (𝑐 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) | 
| 21 | 20 | eqeq2d 2747 | . . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑣 → ((𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺) ↔ (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) | 
| 22 | 19, 21 | imbi12d 344 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝑣 → ((¬ 𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) | 
| 23 | 22 | cbvralvw 3236 | . . . . . . . . . . . 12
⊢
(∀𝑐 ∈
𝐵 (¬ 𝑈 <s 𝑐 → (𝑈 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) | 
| 24 | 17, 23 | bitrdi 287 | . . . . . . . . . . 11
⊢ (𝑏 = 𝑈 → (∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) | 
| 25 | 11, 24 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑏 = 𝑈 → ((𝐺 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))) ↔ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))) | 
| 26 | 25 | rspcev 3621 | . . . . . . . . 9
⊢ ((𝑈 ∈ 𝐵 ∧ (𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑏 ∈ 𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))) | 
| 27 | 7, 8, 9, 26 | syl12anc 836 | . . . . . . . 8
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∃𝑏 ∈ 𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))) | 
| 28 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝐺 → (𝑎 ∈ dom 𝑏 ↔ 𝐺 ∈ dom 𝑏)) | 
| 29 |  | suceq 6449 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝐺 → suc 𝑎 = suc 𝐺) | 
| 30 | 29 | reseq2d 5996 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝐺 → (𝑏 ↾ suc 𝑎) = (𝑏 ↾ suc 𝐺)) | 
| 31 | 29 | reseq2d 5996 | . . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝐺 → (𝑐 ↾ suc 𝑎) = (𝑐 ↾ suc 𝐺)) | 
| 32 | 30, 31 | eqeq12d 2752 | . . . . . . . . . . . . . 14
⊢ (𝑎 = 𝐺 → ((𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎) ↔ (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))) | 
| 33 | 32 | imbi2d 340 | . . . . . . . . . . . . 13
⊢ (𝑎 = 𝐺 → ((¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)) ↔ (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))) | 
| 34 | 33 | ralbidv 3177 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝐺 → (∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)) ↔ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺)))) | 
| 35 | 28, 34 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑎 = 𝐺 → ((𝑎 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎))) ↔ (𝐺 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))) | 
| 36 | 35 | rexbidv 3178 | . . . . . . . . . 10
⊢ (𝑎 = 𝐺 → (∃𝑏 ∈ 𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎))) ↔ ∃𝑏 ∈ 𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))) | 
| 37 | 36 | elabg 3675 | . . . . . . . . 9
⊢ (𝐺 ∈ dom 𝑈 → (𝐺 ∈ {𝑎 ∣ ∃𝑏 ∈ 𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))} ↔ ∃𝑏 ∈ 𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))) | 
| 38 | 8, 37 | syl 17 | . . . . . . . 8
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝐺 ∈ {𝑎 ∣ ∃𝑏 ∈ 𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))} ↔ ∃𝑏 ∈ 𝐵 (𝐺 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝐺) = (𝑐 ↾ suc 𝐺))))) | 
| 39 | 27, 38 | mpbird 257 | . . . . . . 7
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ {𝑎 ∣ ∃𝑏 ∈ 𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))}) | 
| 40 | 2 | noinfdm 27765 | . . . . . . . 8
⊢ (¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = {𝑎 ∣ ∃𝑏 ∈ 𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))}) | 
| 41 | 40 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑇 = {𝑎 ∣ ∃𝑏 ∈ 𝐵 (𝑎 ∈ dom 𝑏 ∧ ∀𝑐 ∈ 𝐵 (¬ 𝑏 <s 𝑐 → (𝑏 ↾ suc 𝑎) = (𝑐 ↾ suc 𝑎)))}) | 
| 42 | 39, 41 | eleqtrrd 2843 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐺 ∈ dom 𝑇) | 
| 43 |  | ordsucss 7839 | . . . . . 6
⊢ (Ord dom
𝑇 → (𝐺 ∈ dom 𝑇 → suc 𝐺 ⊆ dom 𝑇)) | 
| 44 | 6, 42, 43 | sylc 65 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑇) | 
| 45 |  | dfss2 3968 | . . . . 5
⊢ (suc
𝐺 ⊆ dom 𝑇 ↔ (suc 𝐺 ∩ dom 𝑇) = suc 𝐺) | 
| 46 | 44, 45 | sylib 218 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑇) = suc 𝐺) | 
| 47 | 1, 46 | eqtrid 2788 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑇 ↾ suc 𝐺) = suc 𝐺) | 
| 48 |  | dmres 6029 | . . . 4
⊢ dom
(𝑈 ↾ suc 𝐺) = (suc 𝐺 ∩ dom 𝑈) | 
| 49 |  | simp2l 1199 | . . . . . . . . 9
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝐵 ⊆  No
) | 
| 50 | 49, 7 | sseldd 3983 | . . . . . . . 8
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → 𝑈 ∈  No
) | 
| 51 |  | nodmon 27696 | . . . . . . . 8
⊢ (𝑈 ∈ 
No  → dom 𝑈
∈ On) | 
| 52 | 50, 51 | syl 17 | . . . . . . 7
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom 𝑈 ∈ On) | 
| 53 |  | eloni 6393 | . . . . . . 7
⊢ (dom
𝑈 ∈ On → Ord dom
𝑈) | 
| 54 | 52, 53 | syl 17 | . . . . . 6
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Ord dom 𝑈) | 
| 55 |  | ordsucss 7839 | . . . . . 6
⊢ (Ord dom
𝑈 → (𝐺 ∈ dom 𝑈 → suc 𝐺 ⊆ dom 𝑈)) | 
| 56 | 54, 8, 55 | sylc 65 | . . . . 5
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → suc 𝐺 ⊆ dom 𝑈) | 
| 57 |  | dfss2 3968 | . . . . 5
⊢ (suc
𝐺 ⊆ dom 𝑈 ↔ (suc 𝐺 ∩ dom 𝑈) = suc 𝐺) | 
| 58 | 56, 57 | sylib 218 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (suc 𝐺 ∩ dom 𝑈) = suc 𝐺) | 
| 59 | 48, 58 | eqtrid 2788 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑈 ↾ suc 𝐺) = suc 𝐺) | 
| 60 | 47, 59 | eqtr4d 2779 | . 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → dom (𝑇 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺)) | 
| 61 | 47 | eleq2d 2826 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑇 ↾ suc 𝐺) ↔ 𝑎 ∈ suc 𝐺)) | 
| 62 |  | simpl1 1191 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ¬ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥) | 
| 63 |  | simpl2 1192 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉)) | 
| 64 |  | simpl31 1254 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑈 ∈ 𝐵) | 
| 65 | 56 | sselda 3982 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ dom 𝑈) | 
| 66 | 50 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑈 ∈  No
) | 
| 67 | 66, 51 | syl 17 | . . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → dom 𝑈 ∈ On) | 
| 68 |  | simpl32 1255 | . . . . . . . . . . . 12
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝐺 ∈ dom 𝑈) | 
| 69 |  | onelon 6408 | . . . . . . . . . . . 12
⊢ ((dom
𝑈 ∈ On ∧ 𝐺 ∈ dom 𝑈) → 𝐺 ∈ On) | 
| 70 | 67, 68, 69 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝐺 ∈ On) | 
| 71 |  | onsucb 7838 | . . . . . . . . . . 11
⊢ (𝐺 ∈ On ↔ suc 𝐺 ∈ On) | 
| 72 | 70, 71 | sylib 218 | . . . . . . . . . 10
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → suc 𝐺 ∈ On) | 
| 73 |  | eloni 6393 | . . . . . . . . . 10
⊢ (suc
𝐺 ∈ On → Ord suc
𝐺) | 
| 74 | 72, 73 | syl 17 | . . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → Ord suc 𝐺) | 
| 75 |  | simpr 484 | . . . . . . . . 9
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → 𝑎 ∈ suc 𝐺) | 
| 76 |  | ordsucss 7839 | . . . . . . . . 9
⊢ (Ord suc
𝐺 → (𝑎 ∈ suc 𝐺 → suc 𝑎 ⊆ suc 𝐺)) | 
| 77 | 74, 75, 76 | sylc 65 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → suc 𝑎 ⊆ suc 𝐺) | 
| 78 |  | simpl33 1256 | . . . . . . . 8
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))) | 
| 79 |  | reseq1 5990 | . . . . . . . . . . 11
⊢ ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎)) | 
| 80 |  | resabs1 6023 | . . . . . . . . . . . 12
⊢ (suc
𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑈 ↾ suc 𝑎)) | 
| 81 |  | resabs1 6023 | . . . . . . . . . . . 12
⊢ (suc
𝑎 ⊆ suc 𝐺 → ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)) | 
| 82 | 80, 81 | eqeq12d 2752 | . . . . . . . . . . 11
⊢ (suc
𝑎 ⊆ suc 𝐺 → (((𝑈 ↾ suc 𝐺) ↾ suc 𝑎) = ((𝑣 ↾ suc 𝐺) ↾ suc 𝑎) ↔ (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))) | 
| 83 | 79, 82 | imbitrid 244 | . . . . . . . . . 10
⊢ (suc
𝑎 ⊆ suc 𝐺 → ((𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))) | 
| 84 | 83 | imim2d 57 | . . . . . . . . 9
⊢ (suc
𝑎 ⊆ suc 𝐺 → ((¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))) | 
| 85 | 84 | ralimdv 3168 | . . . . . . . 8
⊢ (suc
𝑎 ⊆ suc 𝐺 → (∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))) | 
| 86 | 77, 78, 85 | sylc 65 | . . . . . . 7
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎))) | 
| 87 | 2 | noinffv 27767 | . . . . . . 7
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝑎 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝑎) = (𝑣 ↾ suc 𝑎)))) → (𝑇‘𝑎) = (𝑈‘𝑎)) | 
| 88 | 62, 63, 64, 65, 86, 87 | syl113anc 1383 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → (𝑇‘𝑎) = (𝑈‘𝑎)) | 
| 89 | 75 | fvresd 6925 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑇 ↾ suc 𝐺)‘𝑎) = (𝑇‘𝑎)) | 
| 90 | 75 | fvresd 6925 | . . . . . 6
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑈 ↾ suc 𝐺)‘𝑎) = (𝑈‘𝑎)) | 
| 91 | 88, 89, 90 | 3eqtr4d 2786 | . . . . 5
⊢ (((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) ∧ 𝑎 ∈ suc 𝐺) → ((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)) | 
| 92 | 91 | ex 412 | . . . 4
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ suc 𝐺 → ((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))) | 
| 93 | 61, 92 | sylbid 240 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑎 ∈ dom (𝑇 ↾ suc 𝐺) → ((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎))) | 
| 94 | 93 | ralrimiv 3144 | . 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ∀𝑎 ∈ dom (𝑇 ↾ suc 𝐺)((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)) | 
| 95 |  | nofun 27695 | . . . . 5
⊢ (𝑇 ∈ 
No  → Fun 𝑇) | 
| 96 | 95 | funresd 6608 | . . . 4
⊢ (𝑇 ∈ 
No  → Fun (𝑇
↾ suc 𝐺)) | 
| 97 | 4, 96 | syl 17 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑇 ↾ suc 𝐺)) | 
| 98 |  | nofun 27695 | . . . . 5
⊢ (𝑈 ∈ 
No  → Fun 𝑈) | 
| 99 | 98 | funresd 6608 | . . . 4
⊢ (𝑈 ∈ 
No  → Fun (𝑈
↾ suc 𝐺)) | 
| 100 | 50, 99 | syl 17 | . . 3
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → Fun (𝑈 ↾ suc 𝐺)) | 
| 101 |  | eqfunfv 7055 | . . 3
⊢ ((Fun
(𝑇 ↾ suc 𝐺) ∧ Fun (𝑈 ↾ suc 𝐺)) → ((𝑇 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑇 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑇 ↾ suc 𝐺)((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))) | 
| 102 | 97, 100, 101 | syl2anc 584 | . 2
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → ((𝑇 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺) ↔ (dom (𝑇 ↾ suc 𝐺) = dom (𝑈 ↾ suc 𝐺) ∧ ∀𝑎 ∈ dom (𝑇 ↾ suc 𝐺)((𝑇 ↾ suc 𝐺)‘𝑎) = ((𝑈 ↾ suc 𝐺)‘𝑎)))) | 
| 103 | 60, 94, 102 | mpbir2and 713 | 1
⊢ ((¬
∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ (𝐵 ⊆  No 
∧ 𝐵 ∈ 𝑉) ∧ (𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀𝑣 ∈ 𝐵 (¬ 𝑈 <s 𝑣 → (𝑈 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))) → (𝑇 ↾ suc 𝐺) = (𝑈 ↾ suc 𝐺)) |