Theorem noprefixmo 31848

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
noprefixmo	|- ( A C_ No -> E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )

Distinct variable groups:   u, A, v, x   u, G, v, x

Proof of Theorem noprefixmo

Dummy variables y p are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		reeanv 3107	. . . 4 |- ( E. u e. A E. p e. A ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) <-> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) )
2		simplrr 801	. . . . . . . . . 10 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> p e. A )
3		simplrl 800	. . . . . . . . . 10 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> u e. A )
4	2, 3	ifcld 4131	. . . . . . . . 9 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> if ( u <s p , p , u ) e. A )
5		iftrue 4092	. . . . . . . . . . . 12 |- ( u <s p -> if ( u <s p , p , u ) = p )
6	5	adantr 481	. . . . . . . . . . 11 |- ( ( u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> if ( u <s p , p , u ) = p )
7		simpll 790	. . . . . . . . . . . . . 14 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> A C_ No )
8	7, 3	sseldd 3604	. . . . . . . . . . . . 13 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> u e. No )
9	7, 2	sseldd 3604	. . . . . . . . . . . . 13 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> p e. No )
10		sltso 31827	. . . . . . . . . . . . . 14 |- <s Or No
11		soasym 31657	. . . . . . . . . . . . . 14 |- ( ( <s Or No /\ ( u e. No /\ p e. No ) ) -> ( u <s p -> -. p <s u ) )
12	10, 11	mpan 706	. . . . . . . . . . . . 13 |- ( ( u e. No /\ p e. No ) -> ( u <s p -> -. p <s u ) )
13	8, 9, 12	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( u <s p -> -. p <s u ) )
14	13	impcom 446	. . . . . . . . . . 11 |- ( ( u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. p <s u )
15	6, 14	eqnbrtrd 4671	. . . . . . . . . 10 |- ( ( u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. if ( u <s p , p , u ) <s u )
16		iffalse 4095	. . . . . . . . . . . 12 |- ( -. u <s p -> if ( u <s p , p , u ) = u )
17	16	adantr 481	. . . . . . . . . . 11 |- ( ( -. u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> if ( u <s p , p , u ) = u )
18		sonr 5056	. . . . . . . . . . . . . 14 |- ( ( <s Or No /\ u e. No ) -> -. u <s u )
19	10, 18	mpan 706	. . . . . . . . . . . . 13 |- ( u e. No -> -. u <s u )
20	8, 19	syl 17	. . . . . . . . . . . 12 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> -. u <s u )
21	20	adantl 482	. . . . . . . . . . 11 |- ( ( -. u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. u <s u )
22	17, 21	eqnbrtrd 4671	. . . . . . . . . 10 |- ( ( -. u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. if ( u <s p , p , u ) <s u )
23	15, 22	pm2.61ian 831	. . . . . . . . 9 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> -. if ( u <s p , p , u ) <s u )
24		sonr 5056	. . . . . . . . . . . . . 14 |- ( ( <s Or No /\ p e. No ) -> -. p <s p )
25	10, 24	mpan 706	. . . . . . . . . . . . 13 |- ( p e. No -> -. p <s p )
26	9, 25	syl 17	. . . . . . . . . . . 12 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> -. p <s p )
27	26	adantl 482	. . . . . . . . . . 11 |- ( ( u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. p <s p )
28	6, 27	eqnbrtrd 4671	. . . . . . . . . 10 |- ( ( u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. if ( u <s p , p , u ) <s p )
29		simpl 473	. . . . . . . . . . 11 |- ( ( -. u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. u <s p )
30	17, 29	eqnbrtrd 4671	. . . . . . . . . 10 |- ( ( -. u <s p /\ ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) ) -> -. if ( u <s p , p , u ) <s p )
31	28, 30	pm2.61ian 831	. . . . . . . . 9 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> -. if ( u <s p , p , u ) <s p )
32		simpr1 1067	. . . . . . . . . . . 12 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> if ( u <s p , p , u ) e. A )
33		simprl2 1107	. . . . . . . . . . . . 13 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) )
34	33	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) )
35		simpr2 1068	. . . . . . . . . . . 12 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> -. if ( u <s p , p , u ) <s u )
36		breq1 4656	. . . . . . . . . . . . . . 15 |- ( v = if ( u <s p , p , u ) -> ( v <s u <-> if ( u <s p , p , u ) <s u ) )
37	36	notbid 308	. . . . . . . . . . . . . 14 |- ( v = if ( u <s p , p , u ) -> ( -. v <s u <-> -. if ( u <s p , p , u ) <s u ) )
38		reseq1 5390	. . . . . . . . . . . . . . 15 |- ( v = if ( u <s p , p , u ) -> ( v |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) )
39	38	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( v = if ( u <s p , p , u ) -> ( ( u |` suc G ) = ( v |` suc G ) <-> ( u |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) ) )
40	37, 39	imbi12d 334	. . . . . . . . . . . . 13 |- ( v = if ( u <s p , p , u ) -> ( ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. if ( u <s p , p , u ) <s u -> ( u |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) ) ) )
41	40	rspcv 3305	. . . . . . . . . . . 12 |- ( if ( u <s p , p , u ) e. A -> ( A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) -> ( -. if ( u <s p , p , u ) <s u -> ( u |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) ) ) )
42	32, 34, 35, 41	syl3c 66	. . . . . . . . . . 11 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> ( u |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) )
43		simprr2 1110	. . . . . . . . . . . . 13 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) )
44	43	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) )
45		simpr3 1069	. . . . . . . . . . . 12 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> -. if ( u <s p , p , u ) <s p )
46		breq1 4656	. . . . . . . . . . . . . . 15 |- ( v = if ( u <s p , p , u ) -> ( v <s p <-> if ( u <s p , p , u ) <s p ) )
47	46	notbid 308	. . . . . . . . . . . . . 14 |- ( v = if ( u <s p , p , u ) -> ( -. v <s p <-> -. if ( u <s p , p , u ) <s p ) )
48	38	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( v = if ( u <s p , p , u ) -> ( ( p |` suc G ) = ( v |` suc G ) <-> ( p |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) ) )
49	47, 48	imbi12d 334	. . . . . . . . . . . . 13 |- ( v = if ( u <s p , p , u ) -> ( ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) <-> ( -. if ( u <s p , p , u ) <s p -> ( p |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) ) ) )
50	49	rspcv 3305	. . . . . . . . . . . 12 |- ( if ( u <s p , p , u ) e. A -> ( A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) -> ( -. if ( u <s p , p , u ) <s p -> ( p |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) ) ) )
51	32, 44, 45, 50	syl3c 66	. . . . . . . . . . 11 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> ( p |` suc G ) = ( if ( u <s p , p , u ) |` suc G ) )
52	42, 51	eqtr4d 2659	. . . . . . . . . 10 |- ( ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) /\ ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) ) -> ( u |` suc G ) = ( p |` suc G ) )
53	52	ex 450	. . . . . . . . 9 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( ( if ( u <s p , p , u ) e. A /\ -. if ( u <s p , p , u ) <s u /\ -. if ( u <s p , p , u ) <s p ) -> ( u |` suc G ) = ( p |` suc G ) ) )
54	4, 23, 31, 53	mp3and 1427	. . . . . . . 8 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( u |` suc G ) = ( p |` suc G ) )
55	54	fveq1d 6193	. . . . . . 7 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( ( u |` suc G ) ` G ) = ( ( p |` suc G ) ` G ) )
56		simprl1 1106	. . . . . . . . . 10 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> G e. dom u )
57		sucidg 5803	. . . . . . . . . 10 |- ( G e. dom u -> G e. suc G )
58	56, 57	syl 17	. . . . . . . . 9 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> G e. suc G )
59	58	fvresd 6208	. . . . . . . 8 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( ( u |` suc G ) ` G ) = ( u ` G ) )
60		simprl3 1108	. . . . . . . 8 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( u ` G ) = x )
61	59, 60	eqtrd 2656	. . . . . . 7 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( ( u |` suc G ) ` G ) = x )
62	58	fvresd 6208	. . . . . . . 8 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( ( p |` suc G ) ` G ) = ( p ` G ) )
63		simprr3 1111	. . . . . . . 8 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( p ` G ) = y )
64	62, 63	eqtrd 2656	. . . . . . 7 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> ( ( p |` suc G ) ` G ) = y )
65	55, 61, 64	3eqtr3d 2664	. . . . . 6 |- ( ( ( A C_ No /\ ( u e. A /\ p e. A ) ) /\ ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) ) -> x = y )
66	65	ex 450	. . . . 5 |- ( ( A C_ No /\ ( u e. A /\ p e. A ) ) -> ( ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
67	66	rexlimdvva 3038	. . . 4 |- ( A C_ No -> ( E. u e. A E. p e. A ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
68	1, 67	syl5bir 233	. . 3 |- ( A C_ No -> ( ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
69	68	alrimivv 1856	. 2 |- ( A C_ No -> A. x A. y ( ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
70		eqeq2 2633	. . . . . 6 |- ( x = y -> ( ( u ` G ) = x <-> ( u ` G ) = y ) )
71	70	3anbi3d 1405	. . . . 5 |- ( x = y -> ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) ) )
72	71	rexbidv 3052	. . . 4 |- ( x = y -> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) ) )
73		dmeq 5324	. . . . . . 7 |- ( u = p -> dom u = dom p )
74	73	eleq2d 2687	. . . . . 6 |- ( u = p -> ( G e. dom u <-> G e. dom p ) )
75		breq2 4657	. . . . . . . . 9 |- ( u = p -> ( v <s u <-> v <s p ) )
76	75	notbid 308	. . . . . . . 8 |- ( u = p -> ( -. v <s u <-> -. v <s p ) )
77		reseq1 5390	. . . . . . . . 9 |- ( u = p -> ( u |` suc G ) = ( p |` suc G ) )
78	77	eqeq1d 2624	. . . . . . . 8 |- ( u = p -> ( ( u |` suc G ) = ( v |` suc G ) <-> ( p |` suc G ) = ( v |` suc G ) ) )
79	76, 78	imbi12d 334	. . . . . . 7 |- ( u = p -> ( ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) <-> ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) ) )
80	79	ralbidv 2986	. . . . . 6 |- ( u = p -> ( A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) <-> A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) ) )
81		fveq1 6190	. . . . . . 7 |- ( u = p -> ( u ` G ) = ( p ` G ) )
82	81	eqeq1d 2624	. . . . . 6 |- ( u = p -> ( ( u ` G ) = y <-> ( p ` G ) = y ) )
83	74, 80, 82	3anbi123d 1399	. . . . 5 |- ( u = p -> ( ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) <-> ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) )
84	83	cbvrexv 3172	. . . 4 |- ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = y ) <-> E. p e. A ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) )
85	72, 84	syl6bb 276	. . 3 |- ( x = y -> ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> E. p e. A ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) )
86	85	mo4 2517	. 2 |- ( E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) <-> A. x A. y ( ( E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) /\ E. p e. A ( G e. dom p /\ A. v e. A ( -. v <s p -> ( p |` suc G ) = ( v |` suc G ) ) /\ ( p ` G ) = y ) ) -> x = y ) )
87	69, 86	sylibr 224	1 |- ( A C_ No -> E* x E. u e. A ( G e. dom u /\ A. v e. A ( -. v <s u -> ( u |` suc G ) = ( v |` suc G ) ) /\ ( u ` G ) = x ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   E*wmo 2471   A.wral 2912   E.wrex 2913   C_ wss 3574   ifcif 4086   class class class wbr 4653   Or wor 5034   dom cdm 5114   |` cres 5116   suc csuc 5725   ` cfv 5888   Nocsur 31793   <scslt 31794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-ord 5726  df-on 5727  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896  df-1o 7560  df-2o 7561  df-no 31796  df-slt 31797

This theorem is referenced by:  nosupno  31849  nosupfv  31852