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

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

Proof of Theorem noinfprefixmo
Dummy variables 𝑦 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reeanv 3269 . . . 4 (∃𝑢𝐴𝑝𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) ↔ (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))
2 breq2 5031 . . . . . . . . . . . . 13 (𝑣 = 𝑝 → (𝑢 <s 𝑣𝑢 <s 𝑝))
32notbid 321 . . . . . . . . . . . 12 (𝑣 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑢 <s 𝑝))
4 reseq1 5813 . . . . . . . . . . . . 13 (𝑣 = 𝑝 → (𝑣 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
54eqeq2d 2749 . . . . . . . . . . . 12 (𝑣 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
63, 5imbi12d 348 . . . . . . . . . . 11 (𝑣 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))))
7 simprl2 1220 . . . . . . . . . . . 12 (((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
87adantl 485 . . . . . . . . . . 11 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
9 simprlr 780 . . . . . . . . . . 11 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝑝𝐴)
106, 8, 9rspcdva 3526 . . . . . . . . . 10 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
11 breq2 5031 . . . . . . . . . . . . . 14 (𝑣 = 𝑢 → (𝑝 <s 𝑣𝑝 <s 𝑢))
1211notbid 321 . . . . . . . . . . . . 13 (𝑣 = 𝑢 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑢))
13 reseq1 5813 . . . . . . . . . . . . . 14 (𝑣 = 𝑢 → (𝑣 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))
1413eqeq2d 2749 . . . . . . . . . . . . 13 (𝑣 = 𝑢 → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
1512, 14imbi12d 348 . . . . . . . . . . . 12 (𝑣 = 𝑢 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))))
16 simprr2 1223 . . . . . . . . . . . . 13 (((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
1716adantl 485 . . . . . . . . . . . 12 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
18 simprll 779 . . . . . . . . . . . 12 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝑢𝐴)
1915, 17, 18rspcdva 3526 . . . . . . . . . . 11 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
20 eqcom 2745 . . . . . . . . . . 11 ((𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
2119, 20syl6ib 254 . . . . . . . . . 10 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
22 simpl 486 . . . . . . . . . . . . 13 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝐴 No )
2322, 18sseldd 3876 . . . . . . . . . . . 12 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝑢 No )
2422, 9sseldd 3876 . . . . . . . . . . . 12 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝑝 No )
25 sltso 33512 . . . . . . . . . . . . 13 <s Or No
26 soasym 5468 . . . . . . . . . . . . 13 (( <s Or No ∧ (𝑢 No 𝑝 No )) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
2725, 26mpan 690 . . . . . . . . . . . 12 ((𝑢 No 𝑝 No ) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
2823, 24, 27syl2anc 587 . . . . . . . . . . 11 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
29 imor 852 . . . . . . . . . . 11 ((𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢) ↔ (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
3028, 29sylib 221 . . . . . . . . . 10 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
3110, 21, 30mpjaod 859 . . . . . . . . 9 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
3231fveq1d 6670 . . . . . . . 8 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = ((𝑝 ↾ suc 𝐺)‘𝐺))
33 simprl1 1219 . . . . . . . . . . 11 (((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → 𝐺 ∈ dom 𝑢)
3433adantl 485 . . . . . . . . . 10 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝐺 ∈ dom 𝑢)
35 sucidg 6244 . . . . . . . . . 10 (𝐺 ∈ dom 𝑢𝐺 ∈ suc 𝐺)
3634, 35syl 17 . . . . . . . . 9 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝐺 ∈ suc 𝐺)
3736fvresd 6688 . . . . . . . 8 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = (𝑢𝐺))
3836fvresd 6688 . . . . . . . 8 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → ((𝑝 ↾ suc 𝐺)‘𝐺) = (𝑝𝐺))
3932, 37, 383eqtr3d 2781 . . . . . . 7 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (𝑢𝐺) = (𝑝𝐺))
40 simprl3 1221 . . . . . . . 8 (((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → (𝑢𝐺) = 𝑥)
4140adantl 485 . . . . . . 7 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (𝑢𝐺) = 𝑥)
42 simprr3 1224 . . . . . . . 8 (((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))) → (𝑝𝐺) = 𝑦)
4342adantl 485 . . . . . . 7 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → (𝑝𝐺) = 𝑦)
4439, 41, 433eqtr3d 2781 . . . . . 6 ((𝐴 No ∧ ((𝑢𝐴𝑝𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))) → 𝑥 = 𝑦)
4544expr 460 . . . . 5 ((𝐴 No ∧ (𝑢𝐴𝑝𝐴)) → (((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
4645rexlimdvva 3203 . . . 4 (𝐴 No → (∃𝑢𝐴𝑝𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
471, 46syl5bir 246 . . 3 (𝐴 No → ((∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
4847alrimivv 1934 . 2 (𝐴 No → ∀𝑥𝑦((∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
49 eqeq2 2750 . . . . . 6 (𝑥 = 𝑦 → ((𝑢𝐺) = 𝑥 ↔ (𝑢𝐺) = 𝑦))
50493anbi3d 1443 . . . . 5 (𝑥 = 𝑦 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦)))
5150rexbidv 3206 . . . 4 (𝑥 = 𝑦 → (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦)))
52 dmeq 5740 . . . . . . 7 (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
5352eleq2d 2818 . . . . . 6 (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢𝐺 ∈ dom 𝑝))
54 breq1 5030 . . . . . . . . 9 (𝑢 = 𝑝 → (𝑢 <s 𝑣𝑝 <s 𝑣))
5554notbid 321 . . . . . . . 8 (𝑢 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑝 <s 𝑣))
56 reseq1 5813 . . . . . . . . 9 (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
5756eqeq1d 2740 . . . . . . . 8 (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
5855, 57imbi12d 348 . . . . . . 7 (𝑢 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
5958ralbidv 3109 . . . . . 6 (𝑢 = 𝑝 → (∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
60 fveq1 6667 . . . . . . 7 (𝑢 = 𝑝 → (𝑢𝐺) = (𝑝𝐺))
6160eqeq1d 2740 . . . . . 6 (𝑢 = 𝑝 → ((𝑢𝐺) = 𝑦 ↔ (𝑝𝐺) = 𝑦))
6253, 59, 613anbi123d 1437 . . . . 5 (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))
6362cbvrexvw 3349 . . . 4 (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑦) ↔ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦))
6451, 63bitrdi 290 . . 3 (𝑥 = 𝑦 → (∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)))
6564mo4 2566 . 2 (∃*𝑥𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ↔ ∀𝑥𝑦((∃𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥) ∧ ∃𝑝𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣𝐴𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝𝐺) = 𝑦)) → 𝑥 = 𝑦))
6648, 65sylibr 237 1 (𝐴 No → ∃*𝑥𝑢𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣𝐴𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢𝐺) = 𝑥))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wo 846  w3a 1088  wal 1540   = wceq 1542  wcel 2113  ∃*wmo 2538  wral 3053  wrex 3054  wss 3841   class class class wbr 5027   Or wor 5437  dom cdm 5519  cres 5521  suc csuc 6168  cfv 6333   No csur 33476   <s cslt 33477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-pss 3860  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-tp 4518  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-mpt 5108  df-tr 5134  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-ord 6169  df-on 6170  df-suc 6172  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-fv 6341  df-1o 8124  df-2o 8125  df-no 33479  df-slt 33480
This theorem is referenced by:  noinfno  33554  noinffv  33557
  Copyright terms: Public domain W3C validator