Theorem ordtconnlem1 29970

Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtconn 29971. See also reconnlem1 22629. (Contributed by Thierry Arnoux, 14-Sep-2018.)

Hypotheses

Ref	Expression
ordtconn.x	|- B = ( Base ` K )
ordtconn.l	|- .<_ = ( ( le ` K ) i^i ( B X. B ) )
ordtconn.j	|- J = (ordTop ` .<_ )

Assertion

Ref	Expression
ordtconnlem1	|- ( ( K e. Toset /\ A C_ B ) -> ( ( J ↾t A ) e. Conn -> A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) ) )

Distinct variable groups:   x, r, y, A   B, r, x, y   J, r   K, r, x, y   x, .<_ , y

Allowed substitution hints:   J( x, y)   .<_ ( r)

Proof of Theorem ordtconnlem1

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1843	. . . . 5 |- F/ r ( K e. Toset /\ A C_ B )
2		nfcv 2764	. . . . . . 7 |- F/_ r A
3		nfra2 2946	. . . . . . 7 |- F/ r A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A )
4	2, 3	nfral 2945	. . . . . 6 |- F/ r A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A )
5	4	nfn 1784	. . . . 5 |- F/ r -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A )
6	1, 5	nfan 1828	. . . 4 |- F/ r ( ( K e. Toset /\ A C_ B ) /\ -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
7		tospos 29658	. . . . . . . . . 10 |- ( K e. Toset -> K e. Poset )
8		posprs 16949	. . . . . . . . . 10 |- ( K e. Poset -> K e. Preset )
9		ordtconn.j	. . . . . . . . . . 11 |- J = (ordTop ` .<_ )
10		ordtconn.l	. . . . . . . . . . . . . 14 |- .<_ = ( ( le ` K ) i^i ( B X. B ) )
11		fvex 6201	. . . . . . . . . . . . . . 15 |- ( le ` K ) e. _V
12	11	inex1 4799	. . . . . . . . . . . . . 14 |- ( ( le ` K ) i^i ( B X. B ) ) e. _V
13	10, 12	eqeltri 2697	. . . . . . . . . . . . 13 |- .<_ e. _V
14		eqid 2622	. . . . . . . . . . . . . 14 |- dom .<_ = dom .<_
15	14	ordttopon 20997	. . . . . . . . . . . . 13 |- ( .<_ e. _V -> (ordTop ` .<_ ) e. (TopOn ` dom .<_ ) )
16	13, 15	ax-mp 5	. . . . . . . . . . . 12 |- (ordTop ` .<_ ) e. (TopOn ` dom .<_ )
17		ordtconn.x	. . . . . . . . . . . . . 14 |- B = ( Base ` K )
18	17, 10	prsdm 29960	. . . . . . . . . . . . 13 |- ( K e. Preset -> dom .<_ = B )
19	18	fveq2d 6195	. . . . . . . . . . . 12 |- ( K e. Preset -> (TopOn ` dom .<_ ) = (TopOn ` B ) )
20	16, 19	syl5eleq 2707	. . . . . . . . . . 11 |- ( K e. Preset -> (ordTop ` .<_ ) e. (TopOn ` B ) )
21	9, 20	syl5eqel 2705	. . . . . . . . . 10 |- ( K e. Preset -> J e. (TopOn ` B ) )
22	7, 8, 21	3syl 18	. . . . . . . . 9 |- ( K e. Toset -> J e. (TopOn ` B ) )
23	22	ad3antrrr 766	. . . . . . . 8 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> J e. (TopOn ` B ) )
24	23	adantlr 751	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> J e. (TopOn ` B ) )
25		simpllr 799	. . . . . . . 8 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> A C_ B )
26	25	adantlr 751	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> A C_ B )
27		simpll 790	. . . . . . . . . . . 12 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> K e. Toset )
28	27, 7, 8	3syl 18	. . . . . . . . . . 11 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> K e. Preset )
29		snex 4908	. . . . . . . . . . . . . . . 16 |- { B } e. _V
30		fvex 6201	. . . . . . . . . . . . . . . . . . . 20 |- ( Base ` K ) e. _V
31	17, 30	eqeltri 2697	. . . . . . . . . . . . . . . . . . 19 |- B e. _V
32	31	mptex 6486	. . . . . . . . . . . . . . . . . 18 |- ( x e. B |-> { y e. B | -. y .<_ x } ) e. _V
33	32	rnex 7100	. . . . . . . . . . . . . . . . 17 |- ran ( x e. B |-> { y e. B | -. y .<_ x } ) e. _V
34	31	mptex 6486	. . . . . . . . . . . . . . . . . 18 |- ( x e. B |-> { y e. B | -. x .<_ y } ) e. _V
35	34	rnex 7100	. . . . . . . . . . . . . . . . 17 |- ran ( x e. B |-> { y e. B | -. x .<_ y } ) e. _V
36	33, 35	unex 6956	. . . . . . . . . . . . . . . 16 |- ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) e. _V
37	29, 36	unex 6956	. . . . . . . . . . . . . . 15 |- ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) e. _V
38		ssfii 8325	. . . . . . . . . . . . . . 15 |- ( ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) e. _V -> ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) C_ ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) )
39	37, 38	ax-mp 5	. . . . . . . . . . . . . 14 |- ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) C_ ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) )
40		fvex 6201	. . . . . . . . . . . . . . 15 |- ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) e. _V
41		bastg 20770	. . . . . . . . . . . . . . 15 |- ( ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) e. _V -> ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) C_ ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) ) )
42	40, 41	ax-mp 5	. . . . . . . . . . . . . 14 |- ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) C_ ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) )
43	39, 42	sstri 3612	. . . . . . . . . . . . 13 |- ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) C_ ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) )
44		eqid 2622	. . . . . . . . . . . . . . 15 |- ran ( x e. B |-> { y e. B | -. y .<_ x } ) = ran ( x e. B |-> { y e. B | -. y .<_ x } )
45		eqid 2622	. . . . . . . . . . . . . . 15 |- ran ( x e. B |-> { y e. B | -. x .<_ y } ) = ran ( x e. B |-> { y e. B | -. x .<_ y } )
46	17, 10, 44, 45	ordtprsval 29964	. . . . . . . . . . . . . 14 |- ( K e. Preset -> (ordTop ` .<_ ) = ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) ) )
47	9, 46	syl5eq 2668	. . . . . . . . . . . . 13 |- ( K e. Preset -> J = ( topGen ` ( fi ` ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) ) ) )
48	43, 47	syl5sseqr 3654	. . . . . . . . . . . 12 |- ( K e. Preset -> ( { B } u. ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) ) C_ J )
49	48	unssbd 3791	. . . . . . . . . . 11 |- ( K e. Preset -> ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) C_ J )
50	28, 49	syl 17	. . . . . . . . . 10 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ( ran ( x e. B |-> { y e. B | -. y .<_ x } ) u. ran ( x e. B |-> { y e. B | -. x .<_ y } ) ) C_ J )
51	50	unssbd 3791	. . . . . . . . 9 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ran ( x e. B |-> { y e. B | -. x .<_ y } ) C_ J )
52		breq2 4657	. . . . . . . . . . . . . 14 |- ( z = y -> ( r .<_ z <-> r .<_ y ) )
53	52	notbid 308	. . . . . . . . . . . . 13 |- ( z = y -> ( -. r .<_ z <-> -. r .<_ y ) )
54	53	cbvrabv 3199	. . . . . . . . . . . 12 |- { z e. B | -. r .<_ z } = { y e. B | -. r .<_ y }
55		breq1 4656	. . . . . . . . . . . . . . . 16 |- ( x = r -> ( x .<_ y <-> r .<_ y ) )
56	55	notbid 308	. . . . . . . . . . . . . . 15 |- ( x = r -> ( -. x .<_ y <-> -. r .<_ y ) )
57	56	rabbidv 3189	. . . . . . . . . . . . . 14 |- ( x = r -> { y e. B | -. x .<_ y } = { y e. B | -. r .<_ y } )
58	57	eqeq2d 2632	. . . . . . . . . . . . 13 |- ( x = r -> ( { z e. B | -. r .<_ z } = { y e. B | -. x .<_ y } <-> { z e. B | -. r .<_ z } = { y e. B | -. r .<_ y } ) )
59	58	rspcev 3309	. . . . . . . . . . . 12 |- ( ( r e. B /\ { z e. B | -. r .<_ z } = { y e. B | -. r .<_ y } ) -> E. x e. B { z e. B | -. r .<_ z } = { y e. B | -. x .<_ y } )
60	54, 59	mpan2 707	. . . . . . . . . . 11 |- ( r e. B -> E. x e. B { z e. B | -. r .<_ z } = { y e. B | -. x .<_ y } )
61	31	rabex 4813	. . . . . . . . . . . 12 |- { z e. B | -. r .<_ z } e. _V
62		eqid 2622	. . . . . . . . . . . . 13 |- ( x e. B |-> { y e. B | -. x .<_ y } ) = ( x e. B |-> { y e. B | -. x .<_ y } )
63	62	elrnmpt 5372	. . . . . . . . . . . 12 |- ( { z e. B | -. r .<_ z } e. _V -> ( { z e. B | -. r .<_ z } e. ran ( x e. B |-> { y e. B | -. x .<_ y } ) <-> E. x e. B { z e. B | -. r .<_ z } = { y e. B | -. x .<_ y } ) )
64	61, 63	ax-mp 5	. . . . . . . . . . 11 |- ( { z e. B | -. r .<_ z } e. ran ( x e. B |-> { y e. B | -. x .<_ y } ) <-> E. x e. B { z e. B | -. r .<_ z } = { y e. B | -. x .<_ y } )
65	60, 64	sylibr 224	. . . . . . . . . 10 |- ( r e. B -> { z e. B | -. r .<_ z } e. ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
66	65	adantl 482	. . . . . . . . 9 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> { z e. B | -. r .<_ z } e. ran ( x e. B |-> { y e. B | -. x .<_ y } ) )
67	51, 66	sseldd 3604	. . . . . . . 8 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> { z e. B | -. r .<_ z } e. J )
68	67	ad2antrr 762	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> { z e. B | -. r .<_ z } e. J )
69	50	unssad 3790	. . . . . . . . 9 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ran ( x e. B |-> { y e. B | -. y .<_ x } ) C_ J )
70		breq1 4656	. . . . . . . . . . . . . 14 |- ( z = y -> ( z .<_ r <-> y .<_ r ) )
71	70	notbid 308	. . . . . . . . . . . . 13 |- ( z = y -> ( -. z .<_ r <-> -. y .<_ r ) )
72	71	cbvrabv 3199	. . . . . . . . . . . 12 |- { z e. B | -. z .<_ r } = { y e. B | -. y .<_ r }
73		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( x = r -> ( y .<_ x <-> y .<_ r ) )
74	73	notbid 308	. . . . . . . . . . . . . . 15 |- ( x = r -> ( -. y .<_ x <-> -. y .<_ r ) )
75	74	rabbidv 3189	. . . . . . . . . . . . . 14 |- ( x = r -> { y e. B | -. y .<_ x } = { y e. B | -. y .<_ r } )
76	75	eqeq2d 2632	. . . . . . . . . . . . 13 |- ( x = r -> ( { z e. B | -. z .<_ r } = { y e. B | -. y .<_ x } <-> { z e. B | -. z .<_ r } = { y e. B | -. y .<_ r } ) )
77	76	rspcev 3309	. . . . . . . . . . . 12 |- ( ( r e. B /\ { z e. B | -. z .<_ r } = { y e. B | -. y .<_ r } ) -> E. x e. B { z e. B | -. z .<_ r } = { y e. B | -. y .<_ x } )
78	72, 77	mpan2 707	. . . . . . . . . . 11 |- ( r e. B -> E. x e. B { z e. B | -. z .<_ r } = { y e. B | -. y .<_ x } )
79	31	rabex 4813	. . . . . . . . . . . 12 |- { z e. B | -. z .<_ r } e. _V
80		eqid 2622	. . . . . . . . . . . . 13 |- ( x e. B |-> { y e. B | -. y .<_ x } ) = ( x e. B |-> { y e. B | -. y .<_ x } )
81	80	elrnmpt 5372	. . . . . . . . . . . 12 |- ( { z e. B | -. z .<_ r } e. _V -> ( { z e. B | -. z .<_ r } e. ran ( x e. B |-> { y e. B | -. y .<_ x } ) <-> E. x e. B { z e. B | -. z .<_ r } = { y e. B | -. y .<_ x } ) )
82	79, 81	ax-mp 5	. . . . . . . . . . 11 |- ( { z e. B | -. z .<_ r } e. ran ( x e. B |-> { y e. B | -. y .<_ x } ) <-> E. x e. B { z e. B | -. z .<_ r } = { y e. B | -. y .<_ x } )
83	78, 82	sylibr 224	. . . . . . . . . 10 |- ( r e. B -> { z e. B | -. z .<_ r } e. ran ( x e. B |-> { y e. B | -. y .<_ x } ) )
84	83	adantl 482	. . . . . . . . 9 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> { z e. B | -. z .<_ r } e. ran ( x e. B |-> { y e. B | -. y .<_ x } ) )
85	69, 84	sseldd 3604	. . . . . . . 8 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> { z e. B | -. z .<_ r } e. J )
86	85	ad2antrr 762	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> { z e. B | -. z .<_ r } e. J )
87		simpll 790	. . . . . . . . 9 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> ( ( K e. Toset /\ A C_ B ) /\ r e. B ) )
88		simpr 477	. . . . . . . . 9 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> -. r e. A )
89	87, 88	jca 554	. . . . . . . 8 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) )
90		simplrl 800	. . . . . . . 8 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> E. x e. A -. r .<_ x )
91		ssel 3597	. . . . . . . . . . . . . . 15 |- ( A C_ B -> ( x e. A -> x e. B ) )
92	91	ancrd 577	. . . . . . . . . . . . . 14 |- ( A C_ B -> ( x e. A -> ( x e. B /\ x e. A ) ) )
93	92	anim1d 588	. . . . . . . . . . . . 13 |- ( A C_ B -> ( ( x e. A /\ -. r .<_ x ) -> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) ) )
94	93	impl 650	. . . . . . . . . . . 12 |- ( ( ( A C_ B /\ x e. A ) /\ -. r .<_ x ) -> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) )
95		elin 3796	. . . . . . . . . . . . 13 |- ( x e. ( { z e. B | -. r .<_ z } i^i A ) <-> ( x e. { z e. B | -. r .<_ z } /\ x e. A ) )
96		breq2 4657	. . . . . . . . . . . . . . . 16 |- ( z = x -> ( r .<_ z <-> r .<_ x ) )
97	96	notbid 308	. . . . . . . . . . . . . . 15 |- ( z = x -> ( -. r .<_ z <-> -. r .<_ x ) )
98	97	elrab 3363	. . . . . . . . . . . . . 14 |- ( x e. { z e. B | -. r .<_ z } <-> ( x e. B /\ -. r .<_ x ) )
99	98	anbi1i 731	. . . . . . . . . . . . 13 |- ( ( x e. { z e. B | -. r .<_ z } /\ x e. A ) <-> ( ( x e. B /\ -. r .<_ x ) /\ x e. A ) )
100		an32 839	. . . . . . . . . . . . 13 |- ( ( ( x e. B /\ -. r .<_ x ) /\ x e. A ) <-> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) )
101	95, 99, 100	3bitri 286	. . . . . . . . . . . 12 |- ( x e. ( { z e. B | -. r .<_ z } i^i A ) <-> ( ( x e. B /\ x e. A ) /\ -. r .<_ x ) )
102	94, 101	sylibr 224	. . . . . . . . . . 11 |- ( ( ( A C_ B /\ x e. A ) /\ -. r .<_ x ) -> x e. ( { z e. B | -. r .<_ z } i^i A ) )
103		ne0i 3921	. . . . . . . . . . 11 |- ( x e. ( { z e. B | -. r .<_ z } i^i A ) -> ( { z e. B | -. r .<_ z } i^i A ) =/= (/) )
104	102, 103	syl 17	. . . . . . . . . 10 |- ( ( ( A C_ B /\ x e. A ) /\ -. r .<_ x ) -> ( { z e. B | -. r .<_ z } i^i A ) =/= (/) )
105	25, 104	sylanl1 682	. . . . . . . . 9 |- ( ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) /\ -. r .<_ x ) -> ( { z e. B | -. r .<_ z } i^i A ) =/= (/) )
106	105	r19.29an 3077	. . . . . . . 8 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ E. x e. A -. r .<_ x ) -> ( { z e. B | -. r .<_ z } i^i A ) =/= (/) )
107	89, 90, 106	syl2anc 693	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> ( { z e. B | -. r .<_ z } i^i A ) =/= (/) )
108		simplrr 801	. . . . . . . 8 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> E. y e. A -. y .<_ r )
109		ssel 3597	. . . . . . . . . . . . . . 15 |- ( A C_ B -> ( y e. A -> y e. B ) )
110	109	ancrd 577	. . . . . . . . . . . . . 14 |- ( A C_ B -> ( y e. A -> ( y e. B /\ y e. A ) ) )
111	110	anim1d 588	. . . . . . . . . . . . 13 |- ( A C_ B -> ( ( y e. A /\ -. y .<_ r ) -> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) ) )
112	111	impl 650	. . . . . . . . . . . 12 |- ( ( ( A C_ B /\ y e. A ) /\ -. y .<_ r ) -> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) )
113		elin 3796	. . . . . . . . . . . . 13 |- ( y e. ( { z e. B | -. z .<_ r } i^i A ) <-> ( y e. { z e. B | -. z .<_ r } /\ y e. A ) )
114	71	elrab 3363	. . . . . . . . . . . . . 14 |- ( y e. { z e. B | -. z .<_ r } <-> ( y e. B /\ -. y .<_ r ) )
115	114	anbi1i 731	. . . . . . . . . . . . 13 |- ( ( y e. { z e. B | -. z .<_ r } /\ y e. A ) <-> ( ( y e. B /\ -. y .<_ r ) /\ y e. A ) )
116		an32 839	. . . . . . . . . . . . 13 |- ( ( ( y e. B /\ -. y .<_ r ) /\ y e. A ) <-> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) )
117	113, 115, 116	3bitri 286	. . . . . . . . . . . 12 |- ( y e. ( { z e. B | -. z .<_ r } i^i A ) <-> ( ( y e. B /\ y e. A ) /\ -. y .<_ r ) )
118	112, 117	sylibr 224	. . . . . . . . . . 11 |- ( ( ( A C_ B /\ y e. A ) /\ -. y .<_ r ) -> y e. ( { z e. B | -. z .<_ r } i^i A ) )
119		ne0i 3921	. . . . . . . . . . 11 |- ( y e. ( { z e. B | -. z .<_ r } i^i A ) -> ( { z e. B | -. z .<_ r } i^i A ) =/= (/) )
120	118, 119	syl 17	. . . . . . . . . 10 |- ( ( ( A C_ B /\ y e. A ) /\ -. y .<_ r ) -> ( { z e. B | -. z .<_ r } i^i A ) =/= (/) )
121	25, 120	sylanl1 682	. . . . . . . . 9 |- ( ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) /\ -. y .<_ r ) -> ( { z e. B | -. z .<_ r } i^i A ) =/= (/) )
122	121	r19.29an 3077	. . . . . . . 8 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ E. y e. A -. y .<_ r ) -> ( { z e. B | -. z .<_ r } i^i A ) =/= (/) )
123	89, 108, 122	syl2anc 693	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> ( { z e. B | -. z .<_ r } i^i A ) =/= (/) )
124	17, 10	trleile 29666	. . . . . . . . . . . . . . . 16 |- ( ( K e. Toset /\ r e. B /\ z e. B ) -> ( r .<_ z \/ z .<_ r ) )
125		oran 517	. . . . . . . . . . . . . . . 16 |- ( ( r .<_ z \/ z .<_ r ) <-> -. ( -. r .<_ z /\ -. z .<_ r ) )
126	124, 125	sylib 208	. . . . . . . . . . . . . . 15 |- ( ( K e. Toset /\ r e. B /\ z e. B ) -> -. ( -. r .<_ z /\ -. z .<_ r ) )
127	126	3expa 1265	. . . . . . . . . . . . . 14 |- ( ( ( K e. Toset /\ r e. B ) /\ z e. B ) -> -. ( -. r .<_ z /\ -. z .<_ r ) )
128	127	nrexdv 3001	. . . . . . . . . . . . 13 |- ( ( K e. Toset /\ r e. B ) -> -. E. z e. B ( -. r .<_ z /\ -. z .<_ r ) )
129		rabid 3116	. . . . . . . . . . . . . . . . . 18 |- ( z e. { z e. B | -. r .<_ z } <-> ( z e. B /\ -. r .<_ z ) )
130		rabid 3116	. . . . . . . . . . . . . . . . . 18 |- ( z e. { z e. B | -. z .<_ r } <-> ( z e. B /\ -. z .<_ r ) )
131	129, 130	anbi12i 733	. . . . . . . . . . . . . . . . 17 |- ( ( z e. { z e. B | -. r .<_ z } /\ z e. { z e. B | -. z .<_ r } ) <-> ( ( z e. B /\ -. r .<_ z ) /\ ( z e. B /\ -. z .<_ r ) ) )
132		elin 3796	. . . . . . . . . . . . . . . . 17 |- ( z e. ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) <-> ( z e. { z e. B | -. r .<_ z } /\ z e. { z e. B | -. z .<_ r } ) )
133		anandi 871	. . . . . . . . . . . . . . . . 17 |- ( ( z e. B /\ ( -. r .<_ z /\ -. z .<_ r ) ) <-> ( ( z e. B /\ -. r .<_ z ) /\ ( z e. B /\ -. z .<_ r ) ) )
134	131, 132, 133	3bitr4i 292	. . . . . . . . . . . . . . . 16 |- ( z e. ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) <-> ( z e. B /\ ( -. r .<_ z /\ -. z .<_ r ) ) )
135	134	exbii 1774	. . . . . . . . . . . . . . 15 |- ( E. z z e. ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) <-> E. z ( z e. B /\ ( -. r .<_ z /\ -. z .<_ r ) ) )
136		nfrab1 3122	. . . . . . . . . . . . . . . . 17 |- F/_ z { z e. B | -. r .<_ z }
137		nfrab1 3122	. . . . . . . . . . . . . . . . 17 |- F/_ z { z e. B | -. z .<_ r }
138	136, 137	nfin 3820	. . . . . . . . . . . . . . . 16 |- F/_ z ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } )
139	138	n0f 3927	. . . . . . . . . . . . . . 15 |- ( ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) =/= (/) <-> E. z z e. ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) )
140		df-rex 2918	. . . . . . . . . . . . . . 15 |- ( E. z e. B ( -. r .<_ z /\ -. z .<_ r ) <-> E. z ( z e. B /\ ( -. r .<_ z /\ -. z .<_ r ) ) )
141	135, 139, 140	3bitr4i 292	. . . . . . . . . . . . . 14 |- ( ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) =/= (/) <-> E. z e. B ( -. r .<_ z /\ -. z .<_ r ) )
142	141	necon1bbii 2843	. . . . . . . . . . . . 13 |- ( -. E. z e. B ( -. r .<_ z /\ -. z .<_ r ) <-> ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) = (/) )
143	128, 142	sylib 208	. . . . . . . . . . . 12 |- ( ( K e. Toset /\ r e. B ) -> ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) = (/) )
144	143	adantlr 751	. . . . . . . . . . 11 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) = (/) )
145	144	adantr 481	. . . . . . . . . 10 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) = (/) )
146	145	ineq1d 3813	. . . . . . . . 9 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) i^i A ) = ( (/) i^i A ) )
147		0in 3969	. . . . . . . . 9 |- ( (/) i^i A ) = (/)
148	146, 147	syl6eq 2672	. . . . . . . 8 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) i^i A ) = (/) )
149	148	adantlr 751	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> ( ( { z e. B | -. r .<_ z } i^i { z e. B | -. z .<_ r } ) i^i A ) = (/) )
150		simplr 792	. . . . . . . . . 10 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> r e. B )
151		simpr 477	. . . . . . . . . 10 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> -. r e. A )
152		vex 3203	. . . . . . . . . . . . . . 15 |- r e. _V
153	152	snss 4316	. . . . . . . . . . . . . 14 |- ( r e. B <-> { r } C_ B )
154		eldif 3584	. . . . . . . . . . . . . . . 16 |- ( r e. ( B \ A ) <-> ( r e. B /\ -. r e. A ) )
155	152	snss 4316	. . . . . . . . . . . . . . . 16 |- ( r e. ( B \ A ) <-> { r } C_ ( B \ A ) )
156	154, 155	bitr3i 266	. . . . . . . . . . . . . . 15 |- ( ( r e. B /\ -. r e. A ) <-> { r } C_ ( B \ A ) )
157		ssconb 3743	. . . . . . . . . . . . . . 15 |- ( ( { r } C_ B /\ A C_ B ) -> ( { r } C_ ( B \ A ) <-> A C_ ( B \ { r } ) ) )
158	156, 157	syl5bb 272	. . . . . . . . . . . . . 14 |- ( ( { r } C_ B /\ A C_ B ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
159	153, 158	sylanb 489	. . . . . . . . . . . . 13 |- ( ( r e. B /\ A C_ B ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
160	159	adantl 482	. . . . . . . . . . . 12 |- ( ( K e. Toset /\ ( r e. B /\ A C_ B ) ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
161	160	anass1rs 849	. . . . . . . . . . 11 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
162	161	adantr 481	. . . . . . . . . 10 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( ( r e. B /\ -. r e. A ) <-> A C_ ( B \ { r } ) ) )
163	150, 151, 162	mpbi2and 956	. . . . . . . . 9 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> A C_ ( B \ { r } ) )
164	7	ad3antrrr 766	. . . . . . . . . 10 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> K e. Poset )
165		nfv 1843	. . . . . . . . . . 11 |- F/ z ( K e. Poset /\ r e. B )
166	136, 137	nfun 3769	. . . . . . . . . . 11 |- F/_ z ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } )
167		nfcv 2764	. . . . . . . . . . 11 |- F/_ z ( B \ { r } )
168		ianor 509	. . . . . . . . . . . . . . 15 |- ( -. ( r .<_ z /\ z .<_ r ) <-> ( -. r .<_ z \/ -. z .<_ r ) )
169	17, 10	posrasymb 29657	. . . . . . . . . . . . . . . . 17 |- ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( ( r .<_ z /\ z .<_ r ) <-> r = z ) )
170		equcom 1945	. . . . . . . . . . . . . . . . 17 |- ( r = z <-> z = r )
171	169, 170	syl6bb 276	. . . . . . . . . . . . . . . 16 |- ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( ( r .<_ z /\ z .<_ r ) <-> z = r ) )
172	171	necon3bbid 2831	. . . . . . . . . . . . . . 15 |- ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( -. ( r .<_ z /\ z .<_ r ) <-> z =/= r ) )
173	168, 172	syl5bbr 274	. . . . . . . . . . . . . 14 |- ( ( K e. Poset /\ r e. B /\ z e. B ) -> ( ( -. r .<_ z \/ -. z .<_ r ) <-> z =/= r ) )
174	173	3expia 1267	. . . . . . . . . . . . 13 |- ( ( K e. Poset /\ r e. B ) -> ( z e. B -> ( ( -. r .<_ z \/ -. z .<_ r ) <-> z =/= r ) ) )
175	174	pm5.32d 671	. . . . . . . . . . . 12 |- ( ( K e. Poset /\ r e. B ) -> ( ( z e. B /\ ( -. r .<_ z \/ -. z .<_ r ) ) <-> ( z e. B /\ z =/= r ) ) )
176	129, 130	orbi12i 543	. . . . . . . . . . . . 13 |- ( ( z e. { z e. B | -. r .<_ z } \/ z e. { z e. B | -. z .<_ r } ) <-> ( ( z e. B /\ -. r .<_ z ) \/ ( z e. B /\ -. z .<_ r ) ) )
177		elun 3753	. . . . . . . . . . . . 13 |- ( z e. ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) <-> ( z e. { z e. B | -. r .<_ z } \/ z e. { z e. B | -. z .<_ r } ) )
178		andi 911	. . . . . . . . . . . . 13 |- ( ( z e. B /\ ( -. r .<_ z \/ -. z .<_ r ) ) <-> ( ( z e. B /\ -. r .<_ z ) \/ ( z e. B /\ -. z .<_ r ) ) )
179	176, 177, 178	3bitr4ri 293	. . . . . . . . . . . 12 |- ( ( z e. B /\ ( -. r .<_ z \/ -. z .<_ r ) ) <-> z e. ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) )
180		eldifsn 4317	. . . . . . . . . . . . 13 |- ( z e. ( B \ { r } ) <-> ( z e. B /\ z =/= r ) )
181	180	bicomi 214	. . . . . . . . . . . 12 |- ( ( z e. B /\ z =/= r ) <-> z e. ( B \ { r } ) )
182	175, 179, 181	3bitr3g 302	. . . . . . . . . . 11 |- ( ( K e. Poset /\ r e. B ) -> ( z e. ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) <-> z e. ( B \ { r } ) ) )
183	165, 166, 167, 182	eqrd 3622	. . . . . . . . . 10 |- ( ( K e. Poset /\ r e. B ) -> ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) = ( B \ { r } ) )
184	164, 150, 183	syl2anc 693	. . . . . . . . 9 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) = ( B \ { r } ) )
185	163, 184	sseqtr4d 3642	. . . . . . . 8 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> A C_ ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) )
186	185	adantlr 751	. . . . . . 7 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> A C_ ( { z e. B | -. r .<_ z } u. { z e. B | -. z .<_ r } ) )
187	24, 26, 68, 86, 107, 123, 149, 186	nconnsubb 21226	. . . . . 6 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) /\ -. r e. A ) -> -. ( J ↾t A ) e. Conn )
188	187	anasss 679	. . . . 5 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ ( ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) /\ -. r e. A ) ) -> -. ( J ↾t A ) e. Conn )
189	188	adantllr 755	. . . 4 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) ) /\ r e. B ) /\ ( ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) /\ -. r e. A ) ) -> -. ( J ↾t A ) e. Conn )
190		rexanali 2998	. . . . . . . . . . 11 |- ( E. r e. B ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> -. A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
191	190	rexbii 3041	. . . . . . . . . 10 |- ( E. y e. A E. r e. B ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> E. y e. A -. A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
192		rexcom 3099	. . . . . . . . . 10 |- ( E. y e. A E. r e. B ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> E. r e. B E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) )
193		rexnal 2995	. . . . . . . . . 10 |- ( E. y e. A -. A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) <-> -. A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
194	191, 192, 193	3bitr3i 290	. . . . . . . . 9 |- ( E. r e. B E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> -. A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
195	194	rexbii 3041	. . . . . . . 8 |- ( E. x e. A E. r e. B E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> E. x e. A -. A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
196		rexcom 3099	. . . . . . . 8 |- ( E. x e. A E. r e. B E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> E. r e. B E. x e. A E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) )
197		rexnal 2995	. . . . . . . 8 |- ( E. x e. A -. A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) <-> -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
198	195, 196, 197	3bitr3i 290	. . . . . . 7 |- ( E. r e. B E. x e. A E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) )
199		r19.41v 3089	. . . . . . . . . 10 |- ( E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> ( E. y e. A ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) )
200	199	rexbii 3041	. . . . . . . . 9 |- ( E. x e. A E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> E. x e. A ( E. y e. A ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) )
201		r19.41v 3089	. . . . . . . . 9 |- ( E. x e. A ( E. y e. A ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> ( E. x e. A E. y e. A ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) )
202		reeanv 3107	. . . . . . . . . 10 |- ( E. x e. A E. y e. A ( x .<_ r /\ r .<_ y ) <-> ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) )
203	202	anbi1i 731	. . . . . . . . 9 |- ( ( E. x e. A E. y e. A ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) /\ -. r e. A ) )
204	200, 201, 203	3bitri 286	. . . . . . . 8 |- ( E. x e. A E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) /\ -. r e. A ) )
205	204	rexbii 3041	. . . . . . 7 |- ( E. r e. B E. x e. A E. y e. A ( ( x .<_ r /\ r .<_ y ) /\ -. r e. A ) <-> E. r e. B ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) /\ -. r e. A ) )
206	198, 205	bitr3i 266	. . . . . 6 |- ( -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) <-> E. r e. B ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) /\ -. r e. A ) )
207	27	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> K e. Toset )
208	25	sselda 3603	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> x e. B )
209		simpllr 799	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> r e. B )
210	17, 10	trleile 29666	. . . . . . . . . . . . . 14 |- ( ( K e. Toset /\ x e. B /\ r e. B ) -> ( x .<_ r \/ r .<_ x ) )
211	207, 208, 209, 210	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( x .<_ r \/ r .<_ x ) )
212		simpr 477	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> x e. A )
213		simplr 792	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> -. r e. A )
214		nelne2 2891	. . . . . . . . . . . . . . 15 |- ( ( x e. A /\ -. r e. A ) -> x =/= r )
215	212, 213, 214	syl2anc 693	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> x =/= r )
216	164	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> K e. Poset )
217	17, 10	posrasymb 29657	. . . . . . . . . . . . . . . 16 |- ( ( K e. Poset /\ x e. B /\ r e. B ) -> ( ( x .<_ r /\ r .<_ x ) <-> x = r ) )
218	217	necon3bbid 2831	. . . . . . . . . . . . . . 15 |- ( ( K e. Poset /\ x e. B /\ r e. B ) -> ( -. ( x .<_ r /\ r .<_ x ) <-> x =/= r ) )
219	216, 208, 209, 218	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( -. ( x .<_ r /\ r .<_ x ) <-> x =/= r ) )
220	215, 219	mpbird 247	. . . . . . . . . . . . 13 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> -. ( x .<_ r /\ r .<_ x ) )
221	211, 220	jca 554	. . . . . . . . . . . 12 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( ( x .<_ r \/ r .<_ x ) /\ -. ( x .<_ r /\ r .<_ x ) ) )
222		pm5.17 932	. . . . . . . . . . . 12 |- ( ( ( x .<_ r \/ r .<_ x ) /\ -. ( x .<_ r /\ r .<_ x ) ) <-> ( x .<_ r <-> -. r .<_ x ) )
223	221, 222	sylib 208	. . . . . . . . . . 11 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ x e. A ) -> ( x .<_ r <-> -. r .<_ x ) )
224	223	rexbidva 3049	. . . . . . . . . 10 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( E. x e. A x .<_ r <-> E. x e. A -. r .<_ x ) )
225	27	ad2antrr 762	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> K e. Toset )
226		simpllr 799	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> r e. B )
227	25	sselda 3603	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> y e. B )
228	17, 10	trleile 29666	. . . . . . . . . . . . . 14 |- ( ( K e. Toset /\ r e. B /\ y e. B ) -> ( r .<_ y \/ y .<_ r ) )
229	225, 226, 227, 228	syl3anc 1326	. . . . . . . . . . . . 13 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( r .<_ y \/ y .<_ r ) )
230		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> y e. A )
231		simplr 792	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> -. r e. A )
232		nelne2 2891	. . . . . . . . . . . . . . . 16 |- ( ( y e. A /\ -. r e. A ) -> y =/= r )
233	230, 231, 232	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> y =/= r )
234	233	necomd 2849	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> r =/= y )
235	164	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> K e. Poset )
236	17, 10	posrasymb 29657	. . . . . . . . . . . . . . . 16 |- ( ( K e. Poset /\ r e. B /\ y e. B ) -> ( ( r .<_ y /\ y .<_ r ) <-> r = y ) )
237	236	necon3bbid 2831	. . . . . . . . . . . . . . 15 |- ( ( K e. Poset /\ r e. B /\ y e. B ) -> ( -. ( r .<_ y /\ y .<_ r ) <-> r =/= y ) )
238	235, 226, 227, 237	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( -. ( r .<_ y /\ y .<_ r ) <-> r =/= y ) )
239	234, 238	mpbird 247	. . . . . . . . . . . . 13 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> -. ( r .<_ y /\ y .<_ r ) )
240	229, 239	jca 554	. . . . . . . . . . . 12 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( ( r .<_ y \/ y .<_ r ) /\ -. ( r .<_ y /\ y .<_ r ) ) )
241		pm5.17 932	. . . . . . . . . . . 12 |- ( ( ( r .<_ y \/ y .<_ r ) /\ -. ( r .<_ y /\ y .<_ r ) ) <-> ( r .<_ y <-> -. y .<_ r ) )
242	240, 241	sylib 208	. . . . . . . . . . 11 |- ( ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) /\ y e. A ) -> ( r .<_ y <-> -. y .<_ r ) )
243	242	rexbidva 3049	. . . . . . . . . 10 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( E. y e. A r .<_ y <-> E. y e. A -. y .<_ r ) )
244	224, 243	anbi12d 747	. . . . . . . . 9 |- ( ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) /\ -. r e. A ) -> ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) <-> ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) )
245	244	ex 450	. . . . . . . 8 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ( -. r e. A -> ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) <-> ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) ) ) )
246	245	pm5.32rd 672	. . . . . . 7 |- ( ( ( K e. Toset /\ A C_ B ) /\ r e. B ) -> ( ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) /\ -. r e. A ) <-> ( ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) /\ -. r e. A ) ) )
247	246	rexbidva 3049	. . . . . 6 |- ( ( K e. Toset /\ A C_ B ) -> ( E. r e. B ( ( E. x e. A x .<_ r /\ E. y e. A r .<_ y ) /\ -. r e. A ) <-> E. r e. B ( ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) /\ -. r e. A ) ) )
248	206, 247	syl5bb 272	. . . . 5 |- ( ( K e. Toset /\ A C_ B ) -> ( -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) <-> E. r e. B ( ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) /\ -. r e. A ) ) )
249	248	biimpa 501	. . . 4 |- ( ( ( K e. Toset /\ A C_ B ) /\ -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) ) -> E. r e. B ( ( E. x e. A -. r .<_ x /\ E. y e. A -. y .<_ r ) /\ -. r e. A ) )
250	6, 189, 249	r19.29af 3076	. . 3 |- ( ( ( K e. Toset /\ A C_ B ) /\ -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) ) -> -. ( J ↾t A ) e. Conn )
251	250	ex 450	. 2 |- ( ( K e. Toset /\ A C_ B ) -> ( -. A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) -> -. ( J ↾t A ) e. Conn ) )
252	251	con4d 114	1 |- ( ( K e. Toset /\ A C_ B ) -> ( ( J ↾t A ) e. Conn -> A. x e. A A. y e. A A. r e. B ( ( x .<_ r /\ r .<_ y ) -> r e. A ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   dom cdm 5114   ran crn 5115   ` cfv 5888  (class class class)co 6650   ficfi 8316   Basecbs 15857   lecple 15948   ↾_t crest 16081   topGenctg 16098  ordTopcordt 16159   Preset cpreset 16926   Posetcpo 16940  Tosetctos 17033  TopOnctopon 20715  Conncconn 21214

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-rep 4771  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-reu 2919  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-int 4476  df-iun 4522  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-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-fin 7959  df-fi 8317  df-rest 16083  df-topgen 16104  df-ordt 16161  df-preset 16928  df-poset 16946  df-toset 17034  df-top 20699  df-topon 20716  df-bases 20750  df-cld 20823  df-conn 21215

This theorem is referenced by: (None)