Metamath Proof Explorer


Theorem noinfprefixmo

Description: In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion noinfprefixmo ( 𝐴 No → ∃* 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )

Proof

Step Hyp Ref Expression
1 reeanv ( ∃ 𝑢𝐴𝑝𝐴 ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ↔ ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ∃ 𝑝𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) )
2 breq2 ( 𝑣 = 𝑝 → ( 𝑢 <s 𝑣𝑢 <s 𝑝 ) )
3 2 notbid ( 𝑣 = 𝑝 → ( ¬ 𝑢 <s 𝑣 ↔ ¬ 𝑢 <s 𝑝 ) )
4 reseq1 ( 𝑣 = 𝑝 → ( 𝑣 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) )
5 4 eqeq2d ( 𝑣 = 𝑝 → ( ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) )
6 3 5 imbi12d ( 𝑣 = 𝑝 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑢 <s 𝑝 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) ) )
7 simprl2 ( ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) → ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
8 7 adantl ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
9 simprlr ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝑝𝐴 )
10 6 8 9 rspcdva ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑢 <s 𝑝 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) )
11 breq2 ( 𝑣 = 𝑢 → ( 𝑝 <s 𝑣𝑝 <s 𝑢 ) )
12 11 notbid ( 𝑣 = 𝑢 → ( ¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑢 ) )
13 reseq1 ( 𝑣 = 𝑢 → ( 𝑣 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) )
14 13 eqeq2d ( 𝑣 = 𝑢 → ( ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ) )
15 12 14 imbi12d ( 𝑣 = 𝑢 → ( ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑝 <s 𝑢 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ) ) )
16 simprr2 ( ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) → ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
17 16 adantl ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
18 simprll ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝑢𝐴 )
19 15 17 18 rspcdva ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑝 <s 𝑢 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ) )
20 eqcom ( ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) )
21 19 20 syl6ib ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑝 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) )
22 simpl ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝐴 No )
23 22 18 sseldd ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝑢 No )
24 22 9 sseldd ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝑝 No )
25 sltso <s Or No
26 soasym ( ( <s Or No ∧ ( 𝑢 No 𝑝 No ) ) → ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) )
27 25 26 mpan ( ( 𝑢 No 𝑝 No ) → ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) )
28 23 24 27 syl2anc ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) )
29 imor ( ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) ↔ ( ¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢 ) )
30 28 29 sylib ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢 ) )
31 10 21 30 mpjaod ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) )
32 31 fveq1d ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( ( 𝑢 ↾ suc 𝐺 ) ‘ 𝐺 ) = ( ( 𝑝 ↾ suc 𝐺 ) ‘ 𝐺 ) )
33 simprl1 ( ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) → 𝐺 ∈ dom 𝑢 )
34 33 adantl ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝐺 ∈ dom 𝑢 )
35 sucidg ( 𝐺 ∈ dom 𝑢𝐺 ∈ suc 𝐺 )
36 34 35 syl ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝐺 ∈ suc 𝐺 )
37 36 fvresd ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( ( 𝑢 ↾ suc 𝐺 ) ‘ 𝐺 ) = ( 𝑢𝐺 ) )
38 36 fvresd ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( ( 𝑝 ↾ suc 𝐺 ) ‘ 𝐺 ) = ( 𝑝𝐺 ) )
39 32 37 38 3eqtr3d ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢𝐺 ) = ( 𝑝𝐺 ) )
40 simprl3 ( ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) → ( 𝑢𝐺 ) = 𝑥 )
41 40 adantl ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢𝐺 ) = 𝑥 )
42 simprr3 ( ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) → ( 𝑝𝐺 ) = 𝑦 )
43 42 adantl ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → ( 𝑝𝐺 ) = 𝑦 )
44 39 41 43 3eqtr3d ( ( 𝐴 No ∧ ( ( 𝑢𝐴𝑝𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) ) ) → 𝑥 = 𝑦 )
45 44 expr ( ( 𝐴 No ∧ ( 𝑢𝐴𝑝𝐴 ) ) → ( ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) )
46 45 rexlimdvva ( 𝐴 No → ( ∃ 𝑢𝐴𝑝𝐴 ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) )
47 1 46 syl5bir ( 𝐴 No → ( ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ∃ 𝑝𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) )
48 47 alrimivv ( 𝐴 No → ∀ 𝑥𝑦 ( ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ∃ 𝑝𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) )
49 eqeq2 ( 𝑥 = 𝑦 → ( ( 𝑢𝐺 ) = 𝑥 ↔ ( 𝑢𝐺 ) = 𝑦 ) )
50 49 3anbi3d ( 𝑥 = 𝑦 → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑦 ) ) )
51 50 rexbidv ( 𝑥 = 𝑦 → ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑦 ) ) )
52 dmeq ( 𝑢 = 𝑝 → dom 𝑢 = dom 𝑝 )
53 52 eleq2d ( 𝑢 = 𝑝 → ( 𝐺 ∈ dom 𝑢𝐺 ∈ dom 𝑝 ) )
54 breq1 ( 𝑢 = 𝑝 → ( 𝑢 <s 𝑣𝑝 <s 𝑣 ) )
55 54 notbid ( 𝑢 = 𝑝 → ( ¬ 𝑢 <s 𝑣 ↔ ¬ 𝑝 <s 𝑣 ) )
56 reseq1 ( 𝑢 = 𝑝 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) )
57 56 eqeq1d ( 𝑢 = 𝑝 → ( ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) )
58 55 57 imbi12d ( 𝑢 = 𝑝 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
59 58 ralbidv ( 𝑢 = 𝑝 → ( ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) )
60 fveq1 ( 𝑢 = 𝑝 → ( 𝑢𝐺 ) = ( 𝑝𝐺 ) )
61 60 eqeq1d ( 𝑢 = 𝑝 → ( ( 𝑢𝐺 ) = 𝑦 ↔ ( 𝑝𝐺 ) = 𝑦 ) )
62 53 59 61 3anbi123d ( 𝑢 = 𝑝 → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑦 ) ↔ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) )
63 62 cbvrexvw ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑦 ) ↔ ∃ 𝑝𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) )
64 51 63 bitrdi ( 𝑥 = 𝑦 → ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ∃ 𝑝𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) )
65 64 mo4 ( ∃* 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ↔ ∀ 𝑥𝑦 ( ( ∃ 𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) ∧ ∃ 𝑝𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) )
66 48 65 sylibr ( 𝐴 No → ∃* 𝑥𝑢𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢𝐺 ) = 𝑥 ) )