Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  noprefixmo Structured version   Visualization version   GIF version

Theorem noprefixmo 31822
 Description: In any class of surreals, there is at most one value of the prefix property. (Contributed by Scott Fenton, 26-Nov-2021.)
Assertion
Ref Expression
noprefixmo (𝐴 No → ∃*𝑥𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
Distinct variable groups:   𝑢,𝐴,𝑣,𝑥   𝑢,𝐺,𝑣,𝑥

Proof of Theorem noprefixmo
Dummy variables 𝑦 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reeanv 3102 . . . 4 (∃𝑢𝐴𝑝𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) ↔ (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))
2 simplrr 800 . . . . . . . . . 10 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝑝𝐴)
3 simplrl 799 . . . . . . . . . 10 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝑢𝐴)
42, 3ifcld 4122 . . . . . . . . 9 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴)
5 iftrue 4083 . . . . . . . . . . . 12 (𝑢 <s 𝑝 → if(𝑢 <s 𝑝, 𝑝, 𝑢) = 𝑝)
65adantr 481 . . . . . . . . . . 11 ((𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → if(𝑢 <s 𝑝, 𝑝, 𝑢) = 𝑝)
7 simpll 789 . . . . . . . . . . . . . 14 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝐴 No )
87, 3sseldd 3596 . . . . . . . . . . . . 13 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝑢 No )
97, 2sseldd 3596 . . . . . . . . . . . . 13 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝑝 No )
10 sltso 31801 . . . . . . . . . . . . . 14 <s Or No
11 soasym 31633 . . . . . . . . . . . . . 14 (( <s Or No ∧ (𝑢 No 𝑝 No )) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
1210, 11mpan 705 . . . . . . . . . . . . 13 ((𝑢 No 𝑝 No ) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
138, 9, 12syl2anc 692 . . . . . . . . . . . 12 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
1413impcom 446 . . . . . . . . . . 11 ((𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ 𝑝 <s 𝑢)
156, 14eqnbrtrd 4662 . . . . . . . . . 10 ((𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢)
16 iffalse 4086 . . . . . . . . . . . 12 𝑢 <s 𝑝 → if(𝑢 <s 𝑝, 𝑝, 𝑢) = 𝑢)
1716adantr 481 . . . . . . . . . . 11 ((¬ 𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → if(𝑢 <s 𝑝, 𝑝, 𝑢) = 𝑢)
18 sonr 5046 . . . . . . . . . . . . . 14 (( <s Or No 𝑢 No ) → ¬ 𝑢 <s 𝑢)
1910, 18mpan 705 . . . . . . . . . . . . 13 (𝑢 No → ¬ 𝑢 <s 𝑢)
208, 19syl 17 . . . . . . . . . . . 12 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ¬ 𝑢 <s 𝑢)
2120adantl 482 . . . . . . . . . . 11 ((¬ 𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ 𝑢 <s 𝑢)
2217, 21eqnbrtrd 4662 . . . . . . . . . 10 ((¬ 𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢)
2315, 22pm2.61ian 830 . . . . . . . . 9 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢)
24 sonr 5046 . . . . . . . . . . . . . 14 (( <s Or No 𝑝 No ) → ¬ 𝑝 <s 𝑝)
2510, 24mpan 705 . . . . . . . . . . . . 13 (𝑝 No → ¬ 𝑝 <s 𝑝)
269, 25syl 17 . . . . . . . . . . . 12 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ¬ 𝑝 <s 𝑝)
2726adantl 482 . . . . . . . . . . 11 ((𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ 𝑝 <s 𝑝)
286, 27eqnbrtrd 4662 . . . . . . . . . 10 ((𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)
29 simpl 473 . . . . . . . . . . 11 ((¬ 𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ 𝑢 <s 𝑝)
3017, 29eqnbrtrd 4662 . . . . . . . . . 10 ((¬ 𝑢 <s 𝑝 ∧ ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)
3128, 30pm2.61ian 830 . . . . . . . . 9 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)
32 simpr1 1065 . . . . . . . . . . . 12 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴)
33 simprl2 1105 . . . . . . . . . . . . 13 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
3433adantr 481 . . . . . . . . . . . 12 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
35 simpr2 1066 . . . . . . . . . . . 12 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢)
36 breq1 4647 . . . . . . . . . . . . . . 15 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → (𝑣 <s 𝑢 ↔ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢))
3736notbid 308 . . . . . . . . . . . . . 14 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → (¬ 𝑣 <s 𝑢 ↔ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢))
38 reseq1 5379 . . . . . . . . . . . . . . 15 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → (𝑣 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺))
3938eqeq2d 2630 . . . . . . . . . . . . . 14 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺)))
4037, 39imbi12d 334 . . . . . . . . . . . . 13 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 → (𝑢 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺))))
4140rspcv 3300 . . . . . . . . . . . 12 (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → (¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 → (𝑢 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺))))
4232, 34, 35, 41syl3c 66 . . . . . . . . . . 11 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → (𝑢 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺))
43 simprr2 1108 . . . . . . . . . . . . 13 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
4443adantr 481 . . . . . . . . . . . 12 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
45 simpr3 1067 . . . . . . . . . . . 12 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)
46 breq1 4647 . . . . . . . . . . . . . . 15 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → (𝑣 <s 𝑝 ↔ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝))
4746notbid 308 . . . . . . . . . . . . . 14 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → (¬ 𝑣 <s 𝑝 ↔ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝))
4838eqeq2d 2630 . . . . . . . . . . . . . 14 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺)))
4947, 48imbi12d 334 . . . . . . . . . . . . 13 (𝑣 = if(𝑢 <s 𝑝, 𝑝, 𝑢) → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝 → (𝑝 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺))))
5049rspcv 3300 . . . . . . . . . . . 12 (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 → (∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) → (¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝 → (𝑝 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺))))
5132, 44, 45, 50syl3c 66 . . . . . . . . . . 11 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → (𝑝 ↾ suc 𝐺) = (if(𝑢 <s 𝑝, 𝑝, 𝑢) ↾ suc 𝐺))
5242, 51eqtr4d 2657 . . . . . . . . . 10 ((((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) ∧ (if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝)) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
5352ex 450 . . . . . . . . 9 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ((if(𝑢 <s 𝑝, 𝑝, 𝑢) ∈ 𝐴 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑢 ∧ ¬ if(𝑢 <s 𝑝, 𝑝, 𝑢) <s 𝑝) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
544, 23, 31, 53mp3and 1425 . . . . . . . 8 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
5554fveq1d 6180 . . . . . . 7 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = ((𝑝 ↾ suc 𝐺)‘𝐺))
56 simprl1 1104 . . . . . . . . . 10 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝐺 ∈ dom 𝑢)
57 sucidg 5791 . . . . . . . . . 10 (𝐺 ∈ dom 𝑢𝐺 ∈ suc 𝐺)
5856, 57syl 17 . . . . . . . . 9 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝐺 ∈ suc 𝐺)
5958fvresd 6195 . . . . . . . 8 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = (𝑢𝐺))
60 simprl3 1106 . . . . . . . 8 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → (𝑢𝐺) = 𝑥)
6159, 60eqtrd 2654 . . . . . . 7 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = 𝑥)
6258fvresd 6195 . . . . . . . 8 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ((𝑝 ↾ suc 𝐺)‘𝐺) = (𝑝𝐺))
63 simprr3 1109 . . . . . . . 8 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → (𝑝𝐺) = 𝑦)
6462, 63eqtrd 2654 . . . . . . 7 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ((𝑝 ↾ suc 𝐺)‘𝐺) = 𝑦)
6555, 61, 643eqtr3d 2662 . . . . . 6 (((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝑥 = 𝑦)
6665ex 450 . . . . 5 ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) → (((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
6766rexlimdvva 3034 . . . 4 (𝐴 No → (∃𝑢𝐴𝑝𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
681, 67syl5bir 233 . . 3 (𝐴 No → ((∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
6968alrimivv 1854 . 2 (𝐴 No → ∀𝑥𝑦((∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
70 eqeq2 2631 . . . . . 6 (𝑥 = 𝑦 → ((𝑢𝐺) = 𝑥 ↔ (𝑢𝐺) = 𝑦))
71703anbi3d 1403 . . . . 5 (𝑥 = 𝑦 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦)))
7271rexbidv 3048 . . . 4 (𝑥 = 𝑦 → (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦)))
73 dmeq 5313 . . . . . . 7 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
7473eleq2d 2685 . . . . . 6 (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢𝐺 ∈ dom 𝑝))
75 breq2 4648 . . . . . . . . 9 (𝑢 = 𝑝 → (𝑣 <s 𝑢𝑣 <s 𝑝))
7675notbid 308 . . . . . . . 8 (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
77 reseq1 5379 . . . . . . . . 9 (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
7877eqeq1d 2622 . . . . . . . 8 (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
7976, 78imbi12d 334 . . . . . . 7 (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
8079ralbidv 2983 . . . . . 6 (𝑢 = 𝑝 → (∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
81 fveq1 6177 . . . . . . 7 (𝑢 = 𝑝 → (𝑢𝐺) = (𝑝𝐺))
8281eqeq1d 2622 . . . . . 6 (𝑢 = 𝑝 → ((𝑢𝐺) = 𝑦 ↔ (𝑝𝐺) = 𝑦))
8374, 80, 823anbi123d 1397 . . . . 5 (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))
8483cbvrexv 3167 . . . 4 (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦) ↔ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))
8572, 84syl6bb 276 . . 3 (𝑥 = 𝑦 → (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))
8685mo4 2515 . 2 (∃*𝑥𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∀𝑥𝑦((∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
8769, 86sylibr 224 1 (𝐴 No → ∃*𝑥𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384   ∧ w3a 1036  ∀wal 1479   = wceq 1481   ∈ wcel 1988  ∃*wmo 2469  ∀wral 2909  ∃wrex 2910   ⊆ wss 3567  ifcif 4077   class class class wbr 4644   Or wor 5024  dom cdm 5104   ↾ cres 5106  suc csuc 5713  ‘cfv 5876   No csur 31767
 Copyright terms: Public domain W3C validator