Metamath Proof Explorer


Theorem nosupres

Description: A restriction law for surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Hypothesis nosupres.1 𝑆 = if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
Assertion nosupres ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑆 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) )

Proof

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