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 imbitrdi ⊢ ( ( 𝐴 ⊆ 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 ltsso ⊢ <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 biimtrrid ⊢ ( 𝐴 ⊆ 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 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) )