Theorem noinfprefixmo 27687

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 3213	. . . 4 ⊢ (∃𝑢 ∈ 𝐴 ∃𝑝 ∈ 𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) ↔ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
2		breq2 5079	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑝 → (𝑢 <s 𝑣 ↔ 𝑢 <s 𝑝))
3	2	notbid 320	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑢 <s 𝑝))
4		reseq1 5932	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑝 → (𝑣 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
5	4	eqeq2d 2752	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
6	3, 5	imbi12d 346	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))))
7		simprl2 1227	. . . . . . . . . . . 12 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
8	7	adantl 483	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
9		simprlr 786	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑝 ∈ 𝐴)
10	6, 8, 9	rspcdva 3563	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
11		breq2 5079	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑝 <s 𝑣 ↔ 𝑝 <s 𝑢))
12	11	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑢))
13		reseq1 5932	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))
14	13	eqeq2d 2752	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
15	12, 14	imbi12d 346	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑢 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))))
16		simprr2 1230	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
17	16	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
18		simprll 785	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ 𝐴)
19	15, 17, 18	rspcdva 3563	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
20		eqcom 2748	. . . . . . . . . . 11 ⊢ ((𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
21	19, 20	imbitrdi 253	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
22		simpl 484	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐴 ⊆ No )
23	22, 18	sseldd 3918	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ No )
24	22, 9	sseldd 3918	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑝 ∈ No )
25		ltsso 27662	. . . . . . . . . . . . 13 ⊢ <s Or No
26		soasym 5562	. . . . . . . . . . . . 13 ⊢ (( <s Or No ∧ (𝑢 ∈ No ∧ 𝑝 ∈ No )) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
27	25, 26	mpan 697	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ No ∧ 𝑝 ∈ No ) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
28	23, 24, 27	syl2anc 591	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
29		imor 860	. . . . . . . . . . 11 ⊢ ((𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢) ↔ (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
30	28, 29	sylib 220	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
31	10, 21, 30	mpjaod 867	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
32	31	fveq1d 6833	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = ((𝑝 ↾ suc 𝐺)‘𝐺))
33		simprl1 1226	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → 𝐺 ∈ dom 𝑢)
34	33	adantl 483	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ dom 𝑢)
35		sucidg 6397	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom 𝑢 → 𝐺 ∈ suc 𝐺)
36	34, 35	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ suc 𝐺)
37	36	fvresd 6851	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = (𝑢‘𝐺))
38	36	fvresd 6851	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑝 ↾ suc 𝐺)‘𝐺) = (𝑝‘𝐺))
39	32, 37, 38	3eqtr3d 2784	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢‘𝐺) = (𝑝‘𝐺))
40		simprl3 1228	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → (𝑢‘𝐺) = 𝑥)
41	40	adantl 483	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢‘𝐺) = 𝑥)
42		simprr3 1231	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → (𝑝‘𝐺) = 𝑦)
43	42	adantl 483	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑝‘𝐺) = 𝑦)
44	39, 41, 43	3eqtr3d 2784	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑥 = 𝑦)
45	44	expr 458	. . . . 5 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴)) → (((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
46	45	rexlimdvva 3198	. . . 4 ⊢ (𝐴 ⊆ No → (∃𝑢 ∈ 𝐴 ∃𝑝 ∈ 𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
47	1, 46	biimtrrid 245	. . 3 ⊢ (𝐴 ⊆ No → ((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
48	47	alrimivv 1936	. 2 ⊢ (𝐴 ⊆ No → ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
49		eqeq2 2753	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = 𝑦))
50	49	3anbi3d 1451	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
51	50	rexbidv 3165	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
52		dmeq 5852	. . . . . . 7 ⊢ (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
53	52	eleq2d 2827	. . . . . 6 ⊢ (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑝))
54		breq1 5078	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑢 <s 𝑣 ↔ 𝑝 <s 𝑣))
55	54	notbid 320	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑝 <s 𝑣))
56		reseq1 5932	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
57	56	eqeq1d 2743	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
58	55, 57	imbi12d 346	. . . . . . 7 ⊢ (𝑢 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
59	58	ralbidv 3164	. . . . . 6 ⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
60		fveq1 6830	. . . . . . 7 ⊢ (𝑢 = 𝑝 → (𝑢‘𝐺) = (𝑝‘𝐺))
61	60	eqeq1d 2743	. . . . . 6 ⊢ (𝑢 = 𝑝 → ((𝑢‘𝐺) = 𝑦 ↔ (𝑝‘𝐺) = 𝑦))
62	53, 59, 61	3anbi123d 1445	. . . . 5 ⊢ (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
63	62	cbvrexvw 3220	. . . 4 ⊢ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))
64	51, 63	bitrdi 289	. . 3 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
65	64	mo4 2572	. 2 ⊢ (∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
66	48, 65	sylibr 236	1 ⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∨ wo 854   ∧ w3a 1093  ∀wal 1546   = wceq 1548   ∈ wcel 2121  ∃*wmo 2543  ∀wral 3055  ∃wrex 3065   ⊆ wss 3885   class class class wbr 5075   Or wor 5528  dom cdm 5621   ↾ cres 5623  suc csuc 6316  ‘cfv 6489   No csur 27625   <s clts 27626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-ord 6317  df-on 6318  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-fv 6497  df-1o 8399  df-2o 8400  df-no 27628  df-lts 27629

This theorem is referenced by:  noinfno  27704  noinffv  27707