Metamath Proof Explorer


Theorem nosupfv

Description: The value of surreal supremum when there is no maximum. (Contributed by Scott Fenton, 5-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 nosupfv.1 𝑆 = if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
2 iffalse ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → if ( ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 , ( ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
3 1 2 syl5eq ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦𝑆 = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) )
4 3 fveq1d ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 → ( 𝑆𝐺 ) = ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) )
5 4 3ad2ant1 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑆𝐺 ) = ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) )
6 simp32 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐺 ∈ 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 28 3ad2ant3 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
30 eleq1 ( 𝑦 = 𝐺 → ( 𝑦 ∈ dom 𝑢𝐺 ∈ dom 𝑢 ) )
31 suceq ( 𝑦 = 𝐺 → suc 𝑦 = suc 𝐺 )
32 31 reseq2d ( 𝑦 = 𝐺 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc 𝐺 ) )
33 31 reseq2d ( 𝑦 = 𝐺 → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝐺 ) )
34 32 33 eqeq12d ( 𝑦 = 𝐺 → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
35 34 imbi2d ( 𝑦 = 𝐺 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
36 35 ralbidv ( 𝑦 = 𝐺 → ( ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
37 30 36 anbi12d ( 𝑦 = 𝐺 → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
38 37 rexbidv ( 𝑦 = 𝐺 → ( ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) )
39 6 29 38 elabd ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → 𝐺 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
40 eleq1 ( 𝑔 = 𝐺 → ( 𝑔 ∈ dom 𝑢𝐺 ∈ dom 𝑢 ) )
41 suceq ( 𝑔 = 𝐺 → suc 𝑔 = suc 𝐺 )
42 41 reseq2d ( 𝑔 = 𝐺 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑢 ↾ suc 𝐺 ) )
43 41 reseq2d ( 𝑔 = 𝐺 → ( 𝑣 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝐺 ) )
44 42 43 eqeq12d ( 𝑔 = 𝐺 → ( ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
45 44 imbi2d ( 𝑔 = 𝐺 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
46 45 ralbidv ( 𝑔 = 𝐺 → ( ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ↔ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
47 fveqeq2 ( 𝑔 = 𝐺 → ( ( 𝑢𝑔 ) = 𝑥 ↔ ( 𝑢𝐺 ) = 𝑥 ) )
48 40 46 47 3anbi123d ( 𝑔 = 𝐺 → ( ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) )
49 48 rexbidv ( 𝑔 = 𝐺 → ( ∃ 𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ↔ ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) )
50 49 iotabidv ( 𝑔 = 𝐺 → ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) = ( ℩ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) )
51 eqid ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) )
52 iotaex ( ℩ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) ∈ V
53 50 51 52 fvmpt ( 𝐺 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } → ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) = ( ℩ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) )
54 39 53 syl ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥𝑢𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢𝑔 ) = 𝑥 ) ) ) ‘ 𝐺 ) = ( ℩ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) )
55 simp1 ( ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → 𝑈𝐴 )
56 simp2 ( ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → 𝐺 ∈ dom 𝑈 )
57 simp3 ( ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
58 eqidd ( ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ( 𝑈𝐺 ) = ( 𝑈𝐺 ) )
59 dmeq ( 𝑢 = 𝑈 → dom 𝑢 = dom 𝑈 )
60 59 eleq2d ( 𝑢 = 𝑈 → ( 𝐺 ∈ dom 𝑢𝐺 ∈ dom 𝑈 ) )
61 breq2 ( 𝑢 = 𝑈 → ( 𝑣 <s 𝑢𝑣 <s 𝑈 ) )
62 61 notbid ( 𝑢 = 𝑈 → ( ¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑈 ) )
63 reseq1 ( 𝑢 = 𝑈 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑈 ↾ suc 𝐺 ) )
64 63 eqeq1d ( 𝑢 = 𝑈 → ( ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
65 62 64 imbi12d ( 𝑢 = 𝑈 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
66 65 ralbidv ( 𝑢 = 𝑈 → ( ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
67 fveq1 ( 𝑢 = 𝑈 → ( 𝑢𝐺 ) = ( 𝑈𝐺 ) )
68 67 eqeq1d ( 𝑢 = 𝑈 → ( ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ↔ ( 𝑈𝐺 ) = ( 𝑈𝐺 ) ) )
69 60 66 68 3anbi123d ( 𝑢 = 𝑈 → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) ↔ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑈𝐺 ) = ( 𝑈𝐺 ) ) ) )
70 69 rspcev ( ( 𝑈𝐴 ∧ ( 𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑈𝐺 ) = ( 𝑈𝐺 ) ) ) → ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) )
71 55 56 57 58 70 syl13anc ( ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) )
72 71 3ad2ant3 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) )
73 fvex ( 𝑈𝐺 ) ∈ V
74 eqid ( 𝑢𝐺 ) = ( 𝑢𝐺 )
75 fvex ( 𝑢𝐺 ) ∈ V
76 eqeq2 ( 𝑥 = ( 𝑢𝐺 ) → ( ( 𝑢𝐺 ) = 𝑥 ↔ ( 𝑢𝐺 ) = ( 𝑢𝐺 ) ) )
77 76 3anbi3d ( 𝑥 = ( 𝑢𝐺 ) → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑢𝐺 ) ) ) )
78 75 77 spcev ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑢𝐺 ) ) → ∃ 𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
79 74 78 mp3an3 ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
80 79 reximi ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑢𝐴𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
81 rexcom4 ( ∃ 𝑢𝐴𝑥 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ∃ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
82 80 81 sylib ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
83 28 82 syl ( ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) → ∃ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
84 83 3ad2ant3 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
85 nosupprefixmo ( 𝐴 No → ∃* 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
86 85 adantr ( ( 𝐴 No 𝐴 ∈ V ) → ∃* 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
87 86 3ad2ant2 ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃* 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
88 df-eu ( ∃! 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ( ∃ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ∃* 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) )
89 84 87 88 sylanbrc ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ∃! 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )
90 eqeq2 ( 𝑥 = ( 𝑈𝐺 ) → ( ( 𝑢𝐺 ) = 𝑥 ↔ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) )
91 90 3anbi3d ( 𝑥 = ( 𝑈𝐺 ) → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) ) )
92 91 rexbidv ( 𝑥 = ( 𝑈𝐺 ) → ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) ) )
93 92 iota2 ( ( ( 𝑈𝐺 ) ∈ V ∧ ∃! 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) → ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) ↔ ( ℩ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) = ( 𝑈𝐺 ) ) )
94 73 89 93 sylancr ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = ( 𝑈𝐺 ) ) ↔ ( ℩ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) = ( 𝑈𝐺 ) ) )
95 72 94 mpbid ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( ℩ 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ) = ( 𝑈𝐺 ) )
96 5 54 95 3eqtrd ( ( ¬ ∃ 𝑥𝐴𝑦𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 No 𝐴 ∈ V ) ∧ ( 𝑈𝐴𝐺 ∈ dom 𝑈 ∧ ∀ 𝑣𝐴 ( ¬ 𝑣 <s 𝑈 → ( 𝑈 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) → ( 𝑆𝐺 ) = ( 𝑈𝐺 ) )