Theorem noinfprefixmo 27647

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 3217	. . . 4 ⊢ (∃𝑢 ∈ 𝐴 ∃𝑝 ∈ 𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) ↔ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
2		breq2 5148	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑝 → (𝑢 <s 𝑣 ↔ 𝑢 <s 𝑝))
3	2	notbid 317	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑢 <s 𝑝))
4		reseq1 5974	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑝 → (𝑣 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
5	4	eqeq2d 2736	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
6	3, 5	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))))
7		simprl2 1216	. . . . . . . . . . . 12 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
8	7	adantl 480	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
9		simprlr 778	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑝 ∈ 𝐴)
10	6, 8, 9	rspcdva 3604	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
11		breq2 5148	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑝 <s 𝑣 ↔ 𝑝 <s 𝑢))
12	11	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑢))
13		reseq1 5974	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))
14	13	eqeq2d 2736	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
15	12, 14	imbi12d 343	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑢 → ((¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))))
16		simprr2 1219	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
17	16	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
18		simprll 777	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ 𝐴)
19	15, 17, 18	rspcdva 3604	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
20		eqcom 2732	. . . . . . . . . . 11 ⊢ ((𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
21	19, 20	imbitrdi 250	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
22		simpl 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐴 ⊆ No )
23	22, 18	sseldd 3974	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ No )
24	22, 9	sseldd 3974	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑝 ∈ No )
25		sltso 27622	. . . . . . . . . . . . 13 ⊢ <s Or No
26		soasym 5616	. . . . . . . . . . . . 13 ⊢ (( <s Or No ∧ (𝑢 ∈ No ∧ 𝑝 ∈ No )) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
27	25, 26	mpan 688	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ No ∧ 𝑝 ∈ No ) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
28	23, 24, 27	syl2anc 582	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
29		imor 851	. . . . . . . . . . 11 ⊢ ((𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢) ↔ (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
30	28, 29	sylib 217	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
31	10, 21, 30	mpjaod 858	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
32	31	fveq1d 6892	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = ((𝑝 ↾ suc 𝐺)‘𝐺))
33		simprl1 1215	. . . . . . . . . . 11 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → 𝐺 ∈ dom 𝑢)
34	33	adantl 480	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ dom 𝑢)
35		sucidg 6446	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom 𝑢 → 𝐺 ∈ suc 𝐺)
36	34, 35	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ suc 𝐺)
37	36	fvresd 6910	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = (𝑢‘𝐺))
38	36	fvresd 6910	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑝 ↾ suc 𝐺)‘𝐺) = (𝑝‘𝐺))
39	32, 37, 38	3eqtr3d 2773	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢‘𝐺) = (𝑝‘𝐺))
40		simprl3 1217	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → (𝑢‘𝐺) = 𝑥)
41	40	adantl 480	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢‘𝐺) = 𝑥)
42		simprr3 1220	. . . . . . . 8 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → (𝑝‘𝐺) = 𝑦)
43	42	adantl 480	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑝‘𝐺) = 𝑦)
44	39, 41, 43	3eqtr3d 2773	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑥 = 𝑦)
45	44	expr 455	. . . . 5 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴)) → (((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
46	45	rexlimdvva 3202	. . . 4 ⊢ (𝐴 ⊆ No → (∃𝑢 ∈ 𝐴 ∃𝑝 ∈ 𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
47	1, 46	biimtrrid 242	. . 3 ⊢ (𝐴 ⊆ No → ((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
48	47	alrimivv 1923	. 2 ⊢ (𝐴 ⊆ No → ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
49		eqeq2 2737	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = 𝑦))
50	49	3anbi3d 1438	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
51	50	rexbidv 3169	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
52		dmeq 5901	. . . . . . 7 ⊢ (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
53	52	eleq2d 2811	. . . . . 6 ⊢ (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑝))
54		breq1 5147	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑢 <s 𝑣 ↔ 𝑝 <s 𝑣))
55	54	notbid 317	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → (¬ 𝑢 <s 𝑣 ↔ ¬ 𝑝 <s 𝑣))
56		reseq1 5974	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
57	56	eqeq1d 2727	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
58	55, 57	imbi12d 343	. . . . . . 7 ⊢ (𝑢 = 𝑝 → ((¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
59	58	ralbidv 3168	. . . . . 6 ⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
60		fveq1 6889	. . . . . . 7 ⊢ (𝑢 = 𝑝 → (𝑢‘𝐺) = (𝑝‘𝐺))
61	60	eqeq1d 2727	. . . . . 6 ⊢ (𝑢 = 𝑝 → ((𝑢‘𝐺) = 𝑦 ↔ (𝑝‘𝐺) = 𝑦))
62	53, 59, 61	3anbi123d 1432	. . . . 5 ⊢ (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
63	62	cbvrexvw 3226	. . . 4 ⊢ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))
64	51, 63	bitrdi 286	. . 3 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
65	64	mo4 2554	. 2 ⊢ (∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑝 <s 𝑣 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
66	48, 65	sylibr 233	1 ⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑢 <s 𝑣 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∨ wo 845   ∧ w3a 1084  ∀wal 1531   = wceq 1533   ∈ wcel 2098  ∃*wmo 2526  ∀wral 3051  ∃wrex 3060   ⊆ wss 3941   class class class wbr 5144   Or wor 5584  dom cdm 5673   ↾ cres 5675  suc csuc 6367  ‘cfv 6543   No csur 27586   <s cslt 27587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5295  ax-nul 5302  ax-pr 5424

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-ord 6368  df-on 6369  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-1o 8480  df-2o 8481  df-no 27589  df-slt 27590

This theorem is referenced by:  noinfno  27664  noinffv  27667