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.

Step	Hyp	Ref	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 𝑝))
3	2	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑢 <s 𝑝))
4		reseq1 5813	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑝 → (𝑣 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
5	4	eqeq2d 2749	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
6	3, 5	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))))
7		simprl2 1220	. . . . . . . . . . . 12 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
8	7	adantl 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 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑝 ∈ 𝐴)
10	6, 8, 9	rspcdva 3526	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
11		breq2 5031	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑝 <s 𝑣 ↔ 𝑝 <s 𝑢))
12	11	notbid 321	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑢))
13		reseq1 5813	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))
14	13	eqeq2d 2749	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
15	12, 14	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑢 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))))
16		simprr2 1223	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
17	16	adantl 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 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ 𝐴)
19	15, 17, 18	rspcdva 3526	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
20		eqcom 2745	. . . . . . . . . . 11 ⊢ ((𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
21	19, 20	syl6ib 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 )
23	22, 18	sseldd 3876	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ No )
24	22, 9	sseldd 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 𝑢))
27	25, 26	mpan 690	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ No ∧ 𝑝 ∈ No ) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
28	23, 24, 27	syl2anc 587	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
29		imor 852	. . . . . . . . . . 11 ⊢ ((𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢) ↔ (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
30	28, 29	sylib 221	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
31	10, 21, 30	mpjaod 859	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
32	31	fveq1d 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 𝑢)
34	33	adantl 485	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ dom 𝑢)
35		sucidg 6244	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom 𝑢 → 𝐺 ∈ suc 𝐺)
36	34, 35	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ suc 𝐺)
37	36	fvresd 6688	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = (𝑢‘𝐺))
38	36	fvresd 6688	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑝 ↾ suc 𝐺)‘𝐺) = (𝑝‘𝐺))
39	32, 37, 38	3eqtr3d 2781	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢‘𝐺) = (𝑝‘𝐺))
40		simprl3 1221	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → (𝑢‘𝐺) = 𝑥)
41	40	adantl 485	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢‘𝐺) = 𝑥)
42		simprr3 1224	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → (𝑝‘𝐺) = 𝑦)
43	42	adantl 485	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑝‘𝐺) = 𝑦)
44	39, 41, 43	3eqtr3d 2781	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑥 = 𝑦)
45	44	expr 460	. . . . 5 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴)) → (((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
46	45	rexlimdvva 3203	. . . 4 ⊢ (𝐴 ⊆ No → (∃𝑢 ∈ 𝐴 ∃𝑝 ∈ 𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
47	1, 46	syl5bir 246	. . 3 ⊢ (𝐴 ⊆ No → ((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
48	47	alrimivv 1934	. 2 ⊢ (𝐴 ⊆ No → ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
49		eqeq2 2750	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = 𝑦))
50	49	3anbi3d 1443	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
51	50	rexbidv 3206	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
52		dmeq 5740	. . . . . . 7 ⊢ (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
53	52	eleq2d 2818	. . . . . 6 ⊢ (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑝))
54		breq1 5030	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑢 <s 𝑣 ↔ 𝑝 <s 𝑣))
55	54	notbid 321	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑝 <s 𝑣))
56		reseq1 5813	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
57	56	eqeq1d 2740	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
58	55, 57	imbi12d 348	. . . . . . 7 ⊢ (𝑢 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
59	58	ralbidv 3109	. . . . . 6 ⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
60		fveq1 6667	. . . . . . 7 ⊢ (𝑢 = 𝑝 → (𝑢‘𝐺) = (𝑝‘𝐺))
61	60	eqeq1d 2740	. . . . . 6 ⊢ (𝑢 = 𝑝 → ((𝑢‘𝐺) = 𝑦 ↔ (𝑝‘𝐺) = 𝑦))
62	53, 59, 61	3anbi123d 1437	. . . . 5 ⊢ (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
63	62	cbvrexvw 3349	. . . 4 ⊢ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))
64	51, 63	bitrdi 290	. . 3 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
65	64	mo4 2566	. 2 ⊢ (∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
66	48, 65	sylibr 237	1 ⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))

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