Metamath Proof Explorer

Theorem noinfres

Description: The restriction of surreal infimum when there is no minimum. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Hypothesis noinfres.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion noinfres ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑇 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) )

Proof

Step Hyp Ref Expression
1 noinfres.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 dmres ⊢ dom ( 𝑇 ↾ suc 𝐺 ) = ( suc 𝐺 ∩ dom 𝑇 )
3 1 noinfno ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) → 𝑇 ∈ No )
4 3 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝑇 ∈ No )
5 nodmord ⊢ ( 𝑇 ∈ No → Ord dom 𝑇 )
6 4 5 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → Ord dom 𝑇 )
7 simp31 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝑈 ∈ 𝐵 )
8 simp32 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐺 ∈ dom 𝑈 )
9 simp33 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
10 dmeq ⊢ ( 𝑏 = 𝑈 → dom 𝑏 = dom 𝑈 )
11 10 eleq2d ⊢ ( 𝑏 = 𝑈 → ( 𝐺 ∈ dom 𝑏 ↔ 𝐺 ∈ dom 𝑈 ) )
12 breq1 ⊢ ( 𝑏 = 𝑈 → ( 𝑏 <s 𝑐 ↔ 𝑈 <s 𝑐 ) )
13 12 notbid ⊢ ( 𝑏 = 𝑈 → ( ¬ 𝑏 <s 𝑐 ↔ ¬ 𝑈 <s 𝑐 ) )
14 reseq1 ⊢ ( 𝑏 = 𝑈 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) )
15 14 eqeq1d ⊢ ( 𝑏 = 𝑈 → ( ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ↔ ( 𝑈 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) )
16 13 15 imbi12d ⊢ ( 𝑏 = 𝑈 → ( ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑈 <s 𝑐 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) )
17 16 ralbidv ⊢ ( 𝑏 = 𝑈 → ( ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ↔ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑈 <s 𝑐 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) )
18 breq2 ⊢ ( 𝑐 = 𝑣 → ( 𝑈 <s 𝑐 ↔ 𝑈 <s 𝑣 ) )
19 18 notbid ⊢ ( 𝑐 = 𝑣 → ( ¬ 𝑈 <s 𝑐 ↔ ¬ 𝑈 <s 𝑣 ) )
20 reseq1 ⊢ ( 𝑐 = 𝑣 → ( 𝑐 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) )
21 20 eqeq2d ⊢ ( 𝑐 = 𝑣 → ( ( 𝑈 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ↔ ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
22 19 21 imbi12d ⊢ ( 𝑐 = 𝑣 → ( ( ¬ 𝑈 <s 𝑐 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
23 22 cbvralvw ⊢ ( ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑈 <s 𝑐 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ↔ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
24 17 23 bitrdi ⊢ ( 𝑏 = 𝑈 → ( ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ↔ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
25 11 24 anbi12d ⊢ ( 𝑏 = 𝑈 → ( ( 𝐺 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) ↔ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
26 25 rspcev ⊢ ( ( 𝑈 ∈ 𝐵 ∧ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑏 ∈ 𝐵 ( 𝐺 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) )
27 7 8 9 26 syl12anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑏 ∈ 𝐵 ( 𝐺 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) )
28 eleq1 ⊢ ( 𝑎 = 𝐺 → ( 𝑎 ∈ dom 𝑏 ↔ 𝐺 ∈ dom 𝑏 ) )
29 suceq ⊢ ( 𝑎 = 𝐺 → suc 𝑎 = suc 𝐺 )
30 29 reseq2d ⊢ ( 𝑎 = 𝐺 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑏 ↾ suc 𝐺 ) )
31 29 reseq2d ⊢ ( 𝑎 = 𝐺 → ( 𝑐 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝐺 ) )
32 30 31 eqeq12d ⊢ ( 𝑎 = 𝐺 → ( ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ↔ ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) )
33 32 imbi2d ⊢ ( 𝑎 = 𝐺 → ( ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ↔ ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) )
34 33 ralbidv ⊢ ( 𝑎 = 𝐺 → ( ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ↔ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) )
35 28 34 anbi12d ⊢ ( 𝑎 = 𝐺 → ( ( 𝑎 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ) ↔ ( 𝐺 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) ) )
36 35 rexbidv ⊢ ( 𝑎 = 𝐺 → ( ∃ 𝑏 ∈ 𝐵 ( 𝑎 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ) ↔ ∃ 𝑏 ∈ 𝐵 ( 𝐺 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) ) )
37 36 elabg ⊢ ( 𝐺 ∈ dom 𝑈 → ( 𝐺 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐵 ( 𝑎 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ) } ↔ ∃ 𝑏 ∈ 𝐵 ( 𝐺 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) ) )
38 8 37 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝐺 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐵 ( 𝑎 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ) } ↔ ∃ 𝑏 ∈ 𝐵 ( 𝐺 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝐺 ) = ( 𝑐 ↾ suc 𝐺 ) ) ) ) )
39 27 38 mpbird ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐺 ∈ { 𝑎 ∣ ∃ 𝑏 ∈ 𝐵 ( 𝑎 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ) } )
40 1 noinfdm ⊢ ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 → dom 𝑇 = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐵 ( 𝑎 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ) } )
41 40 3ad2ant1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → dom 𝑇 = { 𝑎 ∣ ∃ 𝑏 ∈ 𝐵 ( 𝑎 ∈ dom 𝑏 ∧ ∀ 𝑐 ∈ 𝐵 ( ¬ 𝑏 <s 𝑐 → ( 𝑏 ↾ suc 𝑎 ) = ( 𝑐 ↾ suc 𝑎 ) ) ) } )
42 39 41 eleqtrrd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐺 ∈ dom 𝑇 )
43 ordsucss ⊢ ( Ord dom 𝑇 → ( 𝐺 ∈ dom 𝑇 → suc 𝐺 ⊆ dom 𝑇 ) )
44 6 42 43 sylc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → suc 𝐺 ⊆ dom 𝑇 )
45 df-ss ⊢ ( suc 𝐺 ⊆ dom 𝑇 ↔ ( suc 𝐺 ∩ dom 𝑇 ) = suc 𝐺 )
46 44 45 sylib ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( suc 𝐺 ∩ dom 𝑇 ) = suc 𝐺 )
47 2 46 syl5eq ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → dom ( 𝑇 ↾ suc 𝐺 ) = suc 𝐺 )
48 dmres ⊢ dom ( 𝑈 ↾ suc 𝐺 ) = ( suc 𝐺 ∩ dom 𝑈 )
49 simp2l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐵 ⊆ No )
50 49 7 sseldd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝑈 ∈ No )
51 nodmon ⊢ ( 𝑈 ∈ No → dom 𝑈 ∈ On )
52 50 51 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → dom 𝑈 ∈ On )
53 eloni ⊢ ( dom 𝑈 ∈ On → Ord dom 𝑈 )
54 52 53 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → Ord dom 𝑈 )
55 ordsucss ⊢ ( Ord dom 𝑈 → ( 𝐺 ∈ dom 𝑈 → suc 𝐺 ⊆ dom 𝑈 ) )
56 54 8 55 sylc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → suc 𝐺 ⊆ dom 𝑈 )
57 df-ss ⊢ ( suc 𝐺 ⊆ dom 𝑈 ↔ ( suc 𝐺 ∩ dom 𝑈 ) = suc 𝐺 )
58 56 57 sylib ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( suc 𝐺 ∩ dom 𝑈 ) = suc 𝐺 )
59 48 58 syl5eq ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → dom ( 𝑈 ↾ suc 𝐺 ) = suc 𝐺 )
60 47 59 eqtr4d ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → dom ( 𝑇 ↾ suc 𝐺 ) = dom ( 𝑈 ↾ suc 𝐺 ) )
61 47 eleq2d ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑎 ∈ dom ( 𝑇 ↾ suc 𝐺 ) ↔ 𝑎 ∈ suc 𝐺 ) )
62 simpl1 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
63 simpl2 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) )
64 simpl31 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → 𝑈 ∈ 𝐵 )
65 56 sselda ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → 𝑎 ∈ dom 𝑈 )
66 50 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → 𝑈 ∈ No )
67 66 51 syl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → dom 𝑈 ∈ On )
68 simpl32 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → 𝐺 ∈ dom 𝑈 )
69 onelon ⊢ ( ( dom 𝑈 ∈ On ∧ 𝐺 ∈ dom 𝑈 ) → 𝐺 ∈ On )
70 67 68 69 syl2anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → 𝐺 ∈ On )
71 sucelon ⊢ ( 𝐺 ∈ On ↔ suc 𝐺 ∈ On )
72 70 71 sylib ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → suc 𝐺 ∈ On )
73 eloni ⊢ ( suc 𝐺 ∈ On → Ord suc 𝐺 )
74 72 73 syl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → Ord suc 𝐺 )
75 simpr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → 𝑎 ∈ suc 𝐺 )
76 ordsucss ⊢ ( Ord suc 𝐺 → ( 𝑎 ∈ suc 𝐺 → suc 𝑎 ⊆ suc 𝐺 ) )
77 74 75 76 sylc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → suc 𝑎 ⊆ suc 𝐺 )
78 simpl33 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
79 reseq1 ⊢ ( ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) → ( ( 𝑈 ↾ suc 𝐺 ) ↾ suc 𝑎 ) = ( ( 𝑣 ↾ suc 𝐺 ) ↾ suc 𝑎 ) )
80 resabs1 ⊢ ( suc 𝑎 ⊆ suc 𝐺 → ( ( 𝑈 ↾ suc 𝐺 ) ↾ suc 𝑎 ) = ( 𝑈 ↾ suc 𝑎 ) )
81 resabs1 ⊢ ( suc 𝑎 ⊆ suc 𝐺 → ( ( 𝑣 ↾ suc 𝐺 ) ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) )
82 80 81 eqeq12d ⊢ ( suc 𝑎 ⊆ suc 𝐺 → ( ( ( 𝑈 ↾ suc 𝐺 ) ↾ suc 𝑎 ) = ( ( 𝑣 ↾ suc 𝐺 ) ↾ suc 𝑎 ) ↔ ( 𝑈 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) )
83 79 82 syl5ib ⊢ ( suc 𝑎 ⊆ suc 𝐺 → ( ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) → ( 𝑈 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) )
84 83 imim2d ⊢ ( suc 𝑎 ⊆ suc 𝐺 → ( ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) → ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
85 84 ralimdv ⊢ ( suc 𝑎 ⊆ suc 𝐺 → ( ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) → ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) )
86 77 78 85 sylc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) )
87 1 noinffv ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝑎 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝑎 ) = ( 𝑣 ↾ suc 𝑎 ) ) ) ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑈 ‘ 𝑎 ) )
88 62 63 64 65 86 87 syl113anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ( 𝑇 ‘ 𝑎 ) = ( 𝑈 ‘ 𝑎 ) )
89 75 fvresd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ( ( 𝑇 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( 𝑇 ‘ 𝑎 ) )
90 75 fvresd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ( ( 𝑈 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( 𝑈 ‘ 𝑎 ) )
91 88 89 90 3eqtr4d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) ∧ 𝑎 ∈ suc 𝐺 ) → ( ( 𝑇 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( ( 𝑈 ↾ suc 𝐺 ) ‘ 𝑎 ) )
92 91 ex ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑎 ∈ suc 𝐺 → ( ( 𝑇 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( ( 𝑈 ↾ suc 𝐺 ) ‘ 𝑎 ) ) )
93 61 92 sylbid ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑎 ∈ dom ( 𝑇 ↾ suc 𝐺 ) → ( ( 𝑇 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( ( 𝑈 ↾ suc 𝐺 ) ‘ 𝑎 ) ) )
94 93 ralrimiv ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∀ 𝑎 ∈ dom ( 𝑇 ↾ suc 𝐺 ) ( ( 𝑇 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( ( 𝑈 ↾ suc 𝐺 ) ‘ 𝑎 ) )
95 nofun ⊢ ( 𝑇 ∈ No → Fun 𝑇 )
96 95 funresd ⊢ ( 𝑇 ∈ No → Fun ( 𝑇 ↾ suc 𝐺 ) )
97 4 96 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → Fun ( 𝑇 ↾ suc 𝐺 ) )
98 nofun ⊢ ( 𝑈 ∈ No → Fun 𝑈 )
99 98 funresd ⊢ ( 𝑈 ∈ No → Fun ( 𝑈 ↾ suc 𝐺 ) )
100 50 99 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → Fun ( 𝑈 ↾ suc 𝐺 ) )
101 eqfunfv ⊢ ( ( Fun ( 𝑇 ↾ suc 𝐺 ) ∧ Fun ( 𝑈 ↾ suc 𝐺 ) ) → ( ( 𝑇 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) ↔ ( dom ( 𝑇 ↾ suc 𝐺 ) = dom ( 𝑈 ↾ suc 𝐺 ) ∧ ∀ 𝑎 ∈ dom ( 𝑇 ↾ suc 𝐺 ) ( ( 𝑇 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( ( 𝑈 ↾ suc 𝐺 ) ‘ 𝑎 ) ) ) )
102 97 100 101 syl2anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( ( 𝑇 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) ↔ ( dom ( 𝑇 ↾ suc 𝐺 ) = dom ( 𝑈 ↾ suc 𝐺 ) ∧ ∀ 𝑎 ∈ dom ( 𝑇 ↾ suc 𝐺 ) ( ( 𝑇 ↾ suc 𝐺 ) ‘ 𝑎 ) = ( ( 𝑈 ↾ suc 𝐺 ) ‘ 𝑎 ) ) ) )
103 60 94 102 mpbir2and ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑈 <s 𝑣 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑇 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) )