Theorem nosupprefixmo 27610

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
nosupprefixmo	⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))

Distinct variable groups:   𝑢,𝐴,𝑣,𝑥   𝑢,𝐺,𝑣,𝑥

Proof of Theorem nosupprefixmo

Dummy variables 𝑦 𝑝 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reeanv 3201	. . . 4 ⊢ (∃𝑢 ∈ 𝐴 ∃𝑝 ∈ 𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) ↔ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
2		breq1 5095	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 <s 𝑝 ↔ 𝑢 <s 𝑝))
3	2	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → (¬ 𝑣 <s 𝑝 ↔ ¬ 𝑢 <s 𝑝))
4		reseq1 5924	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑢 → (𝑣 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))
5	4	eqeq2d 2740	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑢 → ((𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
6	3, 5	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑢 → ((¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑢 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺))))
7		simprr2 1223	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
8	7	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
9		simprll 778	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ 𝐴)
10	6, 8, 9	rspcdva 3578	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺)))
11		eqcom 2736	. . . . . . . . . . 11 ⊢ ((𝑝 ↾ suc 𝐺) = (𝑢 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
12	10, 11	imbitrdi 251	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
13		breq1 5095	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑝 → (𝑣 <s 𝑢 ↔ 𝑝 <s 𝑢))
14	13	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑝 <s 𝑢))
15		reseq1 5924	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑝 → (𝑣 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
16	15	eqeq2d 2740	. . . . . . . . . . . 12 ⊢ (𝑣 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
17	14, 16	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑝 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))))
18		simprl2 1220	. . . . . . . . . . . 12 ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
19	18	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
20		simprlr 779	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑝 ∈ 𝐴)
21	17, 19, 20	rspcdva 3578	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑝 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺)))
22		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐴 ⊆ No )
23	22, 9	sseldd 3936	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑢 ∈ No )
24	22, 20	sseldd 3936	. . . . . . . . . . . 12 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑝 ∈ No )
25		sltso 27586	. . . . . . . . . . . . 13 ⊢ <s Or No
26		soasym 5560	. . . . . . . . . . . . 13 ⊢ (( <s Or No ∧ (𝑢 ∈ No ∧ 𝑝 ∈ No )) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
27	25, 26	mpan 690	. . . . . . . . . . . 12 ⊢ ((𝑢 ∈ No ∧ 𝑝 ∈ No ) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
28	23, 24, 27	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢))
29		pm4.62 856	. . . . . . . . . . 11 ⊢ ((𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢) ↔ (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
30	28, 29	sylib 218	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢))
31	12, 21, 30	mpjaod 860	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
32	31	fveq1d 6824	. . . . . . . 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 481	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ dom 𝑢)
35		sucidg 6390	. . . . . . . . . 10 ⊢ (𝐺 ∈ dom 𝑢 → 𝐺 ∈ suc 𝐺)
36	34, 35	syl 17	. . . . . . . . 9 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝐺 ∈ suc 𝐺)
37	36	fvresd 6842	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑢 ↾ suc 𝐺)‘𝐺) = (𝑢‘𝐺))
38	36	fvresd 6842	. . . . . . . 8 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → ((𝑝 ↾ suc 𝐺)‘𝐺) = (𝑝‘𝐺))
39	32, 37, 38	3eqtr3d 2772	. . . . . . 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 481	. . . . . . 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 481	. . . . . . 7 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → (𝑝‘𝐺) = 𝑦)
44	39, 41, 43	3eqtr3d 2772	. . . . . 6 ⊢ ((𝐴 ⊆ No ∧ ((𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))) → 𝑥 = 𝑦)
45	44	expr 456	. . . . 5 ⊢ ((𝐴 ⊆ No ∧ (𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴)) → (((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
46	45	rexlimdvva 3186	. . . 4 ⊢ (𝐴 ⊆ No → (∃𝑢 ∈ 𝐴 ∃𝑝 ∈ 𝐴 ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
47	1, 46	biimtrrid 243	. . 3 ⊢ (𝐴 ⊆ No → ((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
48	47	alrimivv 1928	. 2 ⊢ (𝐴 ⊆ No → ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
49		eqeq2 2741	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑢‘𝐺) = 𝑥 ↔ (𝑢‘𝐺) = 𝑦))
50	49	3anbi3d 1444	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
51	50	rexbidv 3153	. . . 4 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦)))
52		dmeq 5846	. . . . . . 7 ⊢ (𝑢 = 𝑝 → dom 𝑢 = dom 𝑝)
53	52	eleq2d 2814	. . . . . 6 ⊢ (𝑢 = 𝑝 → (𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑝))
54		breq2 5096	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑣 <s 𝑢 ↔ 𝑣 <s 𝑝))
55	54	notbid 318	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → (¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝))
56		reseq1 5924	. . . . . . . . 9 ⊢ (𝑢 = 𝑝 → (𝑢 ↾ suc 𝐺) = (𝑝 ↾ suc 𝐺))
57	56	eqeq1d 2731	. . . . . . . 8 ⊢ (𝑢 = 𝑝 → ((𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺) ↔ (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)))
58	55, 57	imbi12d 344	. . . . . . 7 ⊢ (𝑢 = 𝑝 → ((¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
59	58	ralbidv 3152	. . . . . 6 ⊢ (𝑢 = 𝑝 → (∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ↔ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺))))
60		fveq1 6821	. . . . . . 7 ⊢ (𝑢 = 𝑝 → (𝑢‘𝐺) = (𝑝‘𝐺))
61	60	eqeq1d 2731	. . . . . 6 ⊢ (𝑢 = 𝑝 → ((𝑢‘𝐺) = 𝑦 ↔ (𝑝‘𝐺) = 𝑦))
62	53, 59, 61	3anbi123d 1438	. . . . 5 ⊢ (𝑢 = 𝑝 → ((𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
63	62	cbvrexvw 3208	. . . 4 ⊢ (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑦) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦))
64	51, 63	bitrdi 287	. . 3 ⊢ (𝑥 = 𝑦 → (∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)))
65	64	mo4 2559	. 2 ⊢ (∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ↔ ∀𝑥∀𝑦((∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥) ∧ ∃𝑝 ∈ 𝐴 (𝐺 ∈ dom 𝑝 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑝 → (𝑝 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑝‘𝐺) = 𝑦)) → 𝑥 = 𝑦))
66	48, 65	sylibr 234	1 ⊢ (𝐴 ⊆ No → ∃*𝑥∃𝑢 ∈ 𝐴 (𝐺 ∈ dom 𝑢 ∧ ∀𝑣 ∈ 𝐴 (¬ 𝑣 <s 𝑢 → (𝑢 ↾ suc 𝐺) = (𝑣 ↾ suc 𝐺)) ∧ (𝑢‘𝐺) = 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1538   = wceq 1540   ∈ wcel 2109  ∃*wmo 2531  ∀wral 3044  ∃wrex 3053   ⊆ wss 3903   class class class wbr 5092   Or wor 5526  dom cdm 5619   ↾ cres 5621  suc csuc 6309  ‘cfv 6482   No csur 27549   <s cslt 27550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-ord 6310  df-on 6311  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490  df-1o 8388  df-2o 8389  df-no 27552  df-slt 27553

This theorem is referenced by:  nosupno  27613  nosupfv  27616