Theorem nosupbnd1lem4

Description: Lemma for nosupbnd1 . If U is a prolongment of S and in A , then ( Udom S ) is not undefined. (Contributed by Scott Fenton, 6-Dec-2021)

	Ref	Expression
Hypothesis	nosupbnd1.1	|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
Assertion	nosupbnd1lem4	|- ( ( -. E. x e. A A. y e. A -. x ( U ` dom S ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		nosupbnd1.1	|- S = if ( E. x e. A A. y e. A -. x . } ) , ( g e. { y | E. u e. A ( y e. dom u /\ A. v e. A ( -. v ( u |` suc y ) = ( v |` suc y ) ) ) } |-> ( iota x E. u e. A ( g e. dom u /\ A. v e. A ( -. v ( u |` suc g ) = ( v |` suc g ) ) /\ ( u ` g ) = x ) ) ) )
2		simpl1	|- ( ( ( -. E. x e. A A. y e. A -. x -. E. x e. A A. y e. A -. x
3		simpl2	|- ( ( ( -. E. x e. A A. y e. A -. x ( A C_ No /\ A e. _V ) )
4		simprl	|- ( ( ( -. E. x e. A A. y e. A -. x w e. A )
5		simpl3	|- ( ( ( -. E. x e. A A. y e. A -. x ( U e. A /\ ( U |` dom S ) = S ) )
6		simprr	|- ( ( ( -. E. x e. A A. y e. A -. x U
7		simp2l	|- ( ( -. E. x e. A A. y e. A -. x A C_ No )
8		simp3l	|- ( ( -. E. x e. A A. y e. A -. x U e. A )
9	7 8	sseldd	|- ( ( -. E. x e. A A. y e. A -. x U e. No )
10		simpl2l	|- ( ( ( -. E. x e. A A. y e. A -. x A C_ No )
11	10 4	sseldd	|- ( ( ( -. E. x e. A A. y e. A -. x w e. No )
12		sltso	|-
13		soasym	|- ( ( ( U -. w
14	12 13	mpan	|- ( ( U e. No /\ w e. No ) -> ( U -. w
15	9 11 14	syl2an2r	|- ( ( ( -. E. x e. A A. y e. A -. x ( U -. w
16	6 15	mpd	|- ( ( ( -. E. x e. A A. y e. A -. x -. w
17	4 16	jca	|- ( ( ( -. E. x e. A A. y e. A -. x ( w e. A /\ -. w
18	1	nosupbnd1lem2	|- ( ( -. E. x e. A A. y e. A -. x ( w |` dom S ) = S )
19	2 3 5 17 18	syl112anc	|- ( ( ( -. E. x e. A A. y e. A -. x ( w |` dom S ) = S )
20	1	nosupbnd1lem3	|- ( ( -. E. x e. A A. y e. A -. x ( w ` dom S ) =/= 2o )
21	2 3 4 19 20	syl112anc	|- ( ( ( -. E. x e. A A. y e. A -. x ( w ` dom S ) =/= 2o )
22	21	neneqd	|- ( ( ( -. E. x e. A A. y e. A -. x -. ( w ` dom S ) = 2o )
23	22	expr	|- ( ( ( -. E. x e. A A. y e. A -. x ( U -. ( w ` dom S ) = 2o ) )
24		imnan	|- ( ( U -. ( w ` dom S ) = 2o ) <-> -. ( U
25	23 24	sylib	|- ( ( ( -. E. x e. A A. y e. A -. x -. ( U
26	25	nrexdv	|- ( ( -. E. x e. A A. y e. A -. x -. E. w e. A ( U
27		simpl3l	|- ( ( ( -. E. x e. A A. y e. A -. x U e. A )
28		simpl1	|- ( ( ( -. E. x e. A A. y e. A -. x -. E. x e. A A. y e. A -. x
29		breq2	|- ( w = y -> ( u u
30	29	cbvrexvw	|- ( E. w e. A u E. y e. A u
31		breq1	|- ( u = x -> ( u x
32	31	rexbidv	|- ( u = x -> ( E. y e. A u E. y e. A x
33	30 32	bitrid	|- ( u = x -> ( E. w e. A u E. y e. A x
34	33	cbvralvw	|- ( A. u e. A E. w e. A u A. x e. A E. y e. A x
35		dfrex2	|- ( E. y e. A x -. A. y e. A -. x
36	35	ralbii	|- ( A. x e. A E. y e. A x A. x e. A -. A. y e. A -. x
37		ralnex	|- ( A. x e. A -. A. y e. A -. x -. E. x e. A A. y e. A -. x
38	34 36 37	3bitri	|- ( A. u e. A E. w e. A u -. E. x e. A A. y e. A -. x
39	28 38	sylibr	|- ( ( ( -. E. x e. A A. y e. A -. x A. u e. A E. w e. A u
40		breq1	|- ( u = U -> ( u U
41	40	rexbidv	|- ( u = U -> ( E. w e. A u E. w e. A U
42	41	rspcv	|- ( U e. A -> ( A. u e. A E. w e. A u E. w e. A U
43	27 39 42	sylc	|- ( ( ( -. E. x e. A A. y e. A -. x E. w e. A U
44		simpl2l	|- ( ( ( -. E. x e. A A. y e. A -. x A C_ No )
45	44 27	sseldd	|- ( ( ( -. E. x e. A A. y e. A -. x U e. No )
46	45	adantr	|- ( ( ( ( -. E. x e. A A. y e. A -. x U e. No )
47	44	adantr	|- ( ( ( ( -. E. x e. A A. y e. A -. x A C_ No )
48		simprl	|- ( ( ( ( -. E. x e. A A. y e. A -. x w e. A )
49	47 48	sseldd	|- ( ( ( ( -. E. x e. A A. y e. A -. x w e. No )
50	1	nosupno	|- ( ( A C_ No /\ A e. _V ) -> S e. No )
51	50	3ad2ant2	|- ( ( -. E. x e. A A. y e. A -. x S e. No )
52	51	adantr	|- ( ( ( -. E. x e. A A. y e. A -. x S e. No )
53	52	adantr	|- ( ( ( ( -. E. x e. A A. y e. A -. x S e. No )
54		nodmon	|- ( S e. No -> dom S e. On )
55	53 54	syl	|- ( ( ( ( -. E. x e. A A. y e. A -. x dom S e. On )
56		simpl3r	|- ( ( ( -. E. x e. A A. y e. A -. x ( U |` dom S ) = S )
57	56	adantr	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( U |` dom S ) = S )
58		simpll1	|- ( ( ( ( -. E. x e. A A. y e. A -. x -. E. x e. A A. y e. A -. x
59		simpll2	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( A C_ No /\ A e. _V ) )
60		simpll3	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( U e. A /\ ( U |` dom S ) = S ) )
61		simprr	|- ( ( ( ( -. E. x e. A A. y e. A -. x U
62	45 49 14	syl2an2r	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( U -. w
63	61 62	mpd	|- ( ( ( ( -. E. x e. A A. y e. A -. x -. w
64	48 63	jca	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( w e. A /\ -. w
65	58 59 60 64 18	syl112anc	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( w |` dom S ) = S )
66	57 65	eqtr4d	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( U |` dom S ) = ( w |` dom S ) )
67		simplr	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( U ` dom S ) = (/) )
68		nolt02o	|- ( ( ( U e. No /\ w e. No /\ dom S e. On ) /\ ( ( U |` dom S ) = ( w |` dom S ) /\ U ( w ` dom S ) = 2o )
69	46 49 55 66 61 67 68	syl321anc	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( w ` dom S ) = 2o )
70	69	expr	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( U ( w ` dom S ) = 2o ) )
71	70	ancld	|- ( ( ( ( -. E. x e. A A. y e. A -. x ( U ( U
72	71	reximdva	|- ( ( ( -. E. x e. A A. y e. A -. x ( E. w e. A U E. w e. A ( U
73	43 72	mpd	|- ( ( ( -. E. x e. A A. y e. A -. x E. w e. A ( U
74	26 73	mtand	|- ( ( -. E. x e. A A. y e. A -. x -. ( U ` dom S ) = (/) )
75	74	neqned	|- ( ( -. E. x e. A A. y e. A -. x ( U ` dom S ) =/= (/) )