Theorem ivthALT 15454

Description: An alternate proof of the Intermediate Value Theorem isupivthi 8552 using topology.

Assertion

Ref	Expression
ivthALT	|- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> E.x e. (A(,)B)(F` x) = U)

Distinct variable groups:   x,A   x,B   x,D   x,F   x,U

Proof of Theorem ivthALT

Step	Hyp	Ref	Expression
1		ssid 2634	. . . . . . . 8 |- CC C_ CC
2		cncff 8528	. . . . . . . 8 |- ((D C_ CC /\ CC C_ CC /\ F e. (D-cn->CC)) -> F:D-->CC)
3	1, 2	mp3an2 1179	. . . . . . 7 |- ((D C_ CC /\ F e. (D-cn->CC)) -> F:D-->CC)
4		ffun 4565	. . . . . . 7 |- (F:D-->CC -> Fun F)
5	3, 4	syl 12	. . . . . 6 |- ((D C_ CC /\ F e. (D-cn->CC)) -> Fun F)
6	5	3ad2antr1 1041	. . . . 5 |- ((D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> Fun F)
7	6	3adant1 894	. . . 4 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> Fun F)
8	7	3ad2ant3 899	. . 3 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> Fun F)
9		iccconn 15453	. . . . . . . . 9 |- ((A e. RR /\ B e. RR) -> (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Con)
10	9	3adant3 896	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ U e. RR) -> (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Con)
11	10	3ad2ant1 897	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Con)
12		retop 8926	. . . . . . . . 9 |- (topGen` ran (,)) e. Top
13	12	a1i 8	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (topGen` ran (,)) e. Top)
14		simp332 1030	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F"(A[,]B)) C_ RR)
15		uniretop 8927	. . . . . . . . 9 |- U.(topGen` ran (,)) = RR
16	14, 15	syl6ssr 2664	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F"(A[,]B)) C_ U.(topGen` ran (,)))
17		stoig3 10253	. . . . . . . 8 |- (((topGen` ran (,)) e. Top /\ (F"(A[,]B)) C_ U.(topGen` ran (,))) -> (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Top)
18	13, 16, 17	syl11anc 524	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Top)
19	3	3ad2antr1 1041	. . . . . . . . . . . 12 |- ((D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> F:D-->CC)
20	19	anim2i 362	. . . . . . . . . . 11 |- (((A[,]B) C_ D /\ (D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((A[,]B) C_ D /\ F:D-->CC))
21	20	3impb 1063	. . . . . . . . . 10 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> ((A[,]B) C_ D /\ F:D-->CC))
22	21	3ad2ant3 899	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((A[,]B) C_ D /\ F:D-->CC))
23	4	adantl 424	. . . . . . . . . 10 |- (((A[,]B) C_ D /\ F:D-->CC) -> Fun F)
24		fdm 4567	. . . . . . . . . . . 12 |- (F:D-->CC -> dom F = D)
25	24	sseq2d 2645	. . . . . . . . . . 11 |- (F:D-->CC -> ((A[,]B) C_ dom F <-> (A[,]B) C_ D))
26	25	biimparc 463	. . . . . . . . . 10 |- (((A[,]B) C_ D /\ F:D-->CC) -> (A[,]B) C_ dom F)
27	23, 26	jca 310	. . . . . . . . 9 |- (((A[,]B) C_ D /\ F:D-->CC) -> (Fun F /\ (A[,]B) C_ dom F))
28		fores 4627	. . . . . . . . 9 |- ((Fun F /\ (A[,]B) C_ dom F) -> (F |` (A[,]B)):(A[,]B)-onto->(F"(A[,]B)))
29	22, 27, 28	3syl 24	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F |` (A[,]B)):(A[,]B)-onto->(F"(A[,]B)))
30		iccssre 7565	. . . . . . . . . . . . 13 |- ((A e. RR /\ B e. RR) -> (A[,]B) C_ RR)
31	30	3adant3 896	. . . . . . . . . . . 12 |- ((A e. RR /\ B e. RR /\ U e. RR) -> (A[,]B) C_ RR)
32	31	3ad2ant1 897	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (A[,]B) C_ RR)
33	32, 15	syl6ssr 2664	. . . . . . . . . 10 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (A[,]B) C_ U.(topGen` ran (,)))
34		stoig2 10252	. . . . . . . . . . 11 |- (((topGen` ran (,)) e. Top /\ (A[,]B) C_ U.(topGen` ran (,))) -> U.(subSp` <.(A[,]B), (topGen` ran (,))>.) = (A[,]B))
35	12, 34	mpan 759	. . . . . . . . . 10 |- ((A[,]B) C_ U.(topGen` ran (,)) -> U.(subSp` <.(A[,]B), (topGen` ran (,))>.) = (A[,]B))
36		foeq2 4614	. . . . . . . . . 10 |- (U.(subSp` <.(A[,]B), (topGen` ran (,))>.) = (A[,]B) -> ((F |` (A[,]B)):U.(subSp` <.(A[,]B), (topGen` ran (,))>.)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) <-> (F |` (A[,]B)):(A[,]B)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.)))
37	33, 35, 36	3syl 24	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((F |` (A[,]B)):U.(subSp` <.(A[,]B), (topGen` ran (,))>.)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) <-> (F |` (A[,]B)):(A[,]B)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.)))
38		stoig2 10252	. . . . . . . . . . 11 |- (((topGen` ran (,)) e. Top /\ (F"(A[,]B)) C_ U.(topGen` ran (,))) -> U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) = (F"(A[,]B)))
39	12, 38	mpan 759	. . . . . . . . . 10 |- ((F"(A[,]B)) C_ U.(topGen` ran (,)) -> U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) = (F"(A[,]B)))
40		foeq3 4615	. . . . . . . . . 10 |- (U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) = (F"(A[,]B)) -> ((F |` (A[,]B)):(A[,]B)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) <-> (F |` (A[,]B)):(A[,]B)-onto->(F"(A[,]B))))
41	16, 39, 40	3syl 24	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((F |` (A[,]B)):(A[,]B)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) <-> (F |` (A[,]B)):(A[,]B)-onto->(F"(A[,]B))))
42	37, 41	bitrd 587	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((F |` (A[,]B)):U.(subSp` <.(A[,]B), (topGen` ran (,))>.)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) <-> (F |` (A[,]B)):(A[,]B)-onto->(F"(A[,]B))))
43	29, 42	mpbird 213	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F |` (A[,]B)):U.(subSp` <.(A[,]B), (topGen` ran (,))>.)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.))
44		eqid 1884	. . . . . . . . . . . . . . 15 |- (abs o. - ) = (abs o. - )
45	44	cnmet 9182	. . . . . . . . . . . . . 14 |- (abs o. - ) e. Met
46		eqid 1884	. . . . . . . . . . . . . . 15 |- (Open` (abs o. - )) = (Open` (abs o. - ))
47	46	opntop 9147	. . . . . . . . . . . . . 14 |- ((abs o. - ) e. Met -> (Open` (abs o. - )) e. Top)
48	45, 47	ax-mp 7	. . . . . . . . . . . . 13 |- (Open` (abs o. - )) e. Top
49	48	a1i 8	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (Open` (abs o. - )) e. Top)
50		simp2 877	. . . . . . . . . . . . . 14 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> D C_ CC)
51	50	3ad2ant3 899	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> D C_ CC)
52	44	cnmetba 9181	. . . . . . . . . . . . . . 15 |- CC = dom dom (abs o. - )
53	52, 46	uniopn2 9138	. . . . . . . . . . . . . 14 |- ((abs o. - ) e. Met -> U.(Open` (abs o. - )) = CC)
54	45, 53	ax-mp 7	. . . . . . . . . . . . 13 |- U.(Open` (abs o. - )) = CC
55	51, 54	syl6ssr 2664	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> D C_ U.(Open` (abs o. - )))
56		stoig3 10253	. . . . . . . . . . . 12 |- (((Open` (abs o. - )) e. Top /\ D C_ U.(Open` (abs o. - ))) -> (subSp` <.D, (Open` (abs o. - ))>.) e. Top)
57	49, 55, 56	syl11anc 524	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.D, (Open` (abs o. - ))>.) e. Top)
58		simp1 876	. . . . . . . . . . . . 13 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> (A[,]B) C_ D)
59	58	3ad2ant3 899	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (A[,]B) C_ D)
60		stoig2 10252	. . . . . . . . . . . . 13 |- (((Open` (abs o. - )) e. Top /\ D C_ U.(Open` (abs o. - ))) -> U.(subSp` <.D, (Open` (abs o. - ))>.) = D)
61	49, 55, 60	syl11anc 524	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U.(subSp` <.D, (Open` (abs o. - ))>.) = D)
62	59, 61	sseqtr4d 2654	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (A[,]B) C_ U.(subSp` <.D, (Open` (abs o. - ))>.))
63		simp331 1029	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> F e. (D-cn->CC))
64		eqid 1884	. . . . . . . . . . . . . . . . 17 |- ((abs o. - ) |` (D X. D)) = ((abs o. - ) |` (D X. D))
65		relco 4392	. . . . . . . . . . . . . . . . . . 19 |- Rel (abs o. - )
66	52	metf 9084	. . . . . . . . . . . . . . . . . . . . . 22 |- ((abs o. - ) e. Met -> (abs o. - ):(CC X. CC)-->RR)
67		fdm 4567	. . . . . . . . . . . . . . . . . . . . . 22 |- ((abs o. - ):(CC X. CC)-->RR -> dom (abs o. - ) = (CC X. CC))
68	66, 67	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- ((abs o. - ) e. Met -> dom (abs o. - ) = (CC X. CC))
69	45, 68	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 |- dom (abs o. - ) = (CC X. CC)
70	69	eqimssi 2668	. . . . . . . . . . . . . . . . . . 19 |- dom (abs o. - ) C_ (CC X. CC)
71		relssres 4248	. . . . . . . . . . . . . . . . . . 19 |- ((Rel (abs o. - ) /\ dom (abs o. - ) C_ (CC X. CC)) -> ((abs o. - ) |` (CC X. CC)) = (abs o. - ))
72	65, 70, 71	mp2an 761	. . . . . . . . . . . . . . . . . 18 |- ((abs o. - ) |` (CC X. CC)) = (abs o. - )
73	72	eqcomi 1888	. . . . . . . . . . . . . . . . 17 |- (abs o. - ) = ((abs o. - ) |` (CC X. CC))
74		eqid 1884	. . . . . . . . . . . . . . . . 17 |- (Open` ((abs o. - ) |` (D X. D))) = (Open` ((abs o. - ) |` (D X. D)))
75	64, 73, 74, 46	cncfmet 9183	. . . . . . . . . . . . . . . 16 |- ((D C_ CC /\ CC C_ CC) -> (D-cn->CC) = ((Open` ((abs o. - ) |` (D X. D))) Cn (Open` (abs o. - ))))
76	1, 75	mpan2 760	. . . . . . . . . . . . . . 15 |- (D C_ CC -> (D-cn->CC) = ((Open` ((abs o. - ) |` (D X. D))) Cn (Open` (abs o. - ))))
77	76	3ad2ant2 898	. . . . . . . . . . . . . 14 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> (D-cn->CC) = ((Open` ((abs o. - ) |` (D X. D))) Cn (Open` (abs o. - ))))
78	77	3ad2ant3 899	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (D-cn->CC) = ((Open` ((abs o. - ) |` (D X. D))) Cn (Open` (abs o. - ))))
79	45	a1i 8	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (abs o. - ) e. Met)
80	64, 52, 46, 74	subtopmet 10256	. . . . . . . . . . . . . . 15 |- (((abs o. - ) e. Met /\ D C_ CC) -> (subSp` <.D, (Open` (abs o. - ))>.) = (Open` ((abs o. - ) |` (D X. D))))
81	79, 51, 80	syl11anc 524	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.D, (Open` (abs o. - ))>.) = (Open` ((abs o. - ) |` (D X. D))))
82	81	opreq1d 4897	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((subSp` <.D, (Open` (abs o. - ))>.) Cn (Open` (abs o. - ))) = ((Open` ((abs o. - ) |` (D X. D))) Cn (Open` (abs o. - ))))
83	78, 82	eqtr4d 1928	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (D-cn->CC) = ((subSp` <.D, (Open` (abs o. - ))>.) Cn (Open` (abs o. - ))))
84	63, 83	eleqtrd 1973	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> F e. ((subSp` <.D, (Open` (abs o. - ))>.) Cn (Open` (abs o. - ))))
85		eqid 1884	. . . . . . . . . . . 12 |- U.(subSp` <.D, (Open` (abs o. - ))>.) = U.(subSp` <.D, (Open` (abs o. - ))>.)
86	85	cnsubsp 15426	. . . . . . . . . . 11 |- ((((subSp` <.D, (Open` (abs o. - ))>.) e. Top /\ (Open` (abs o. - )) e. Top) /\ ((A[,]B) C_ U.(subSp` <.D, (Open` (abs o. - ))>.) /\ F e. ((subSp` <.D, (Open` (abs o. - ))>.) Cn (Open` (abs o. - ))))) -> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (Open` (abs o. - ))))
87	57, 49, 62, 84, 86	syl22anc 1101	. . . . . . . . . 10 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (Open` (abs o. - ))))
88		stoig3 10253	. . . . . . . . . . . 12 |- (((subSp` <.D, (Open` (abs o. - ))>.) e. Top /\ (A[,]B) C_ U.(subSp` <.D, (Open` (abs o. - ))>.)) -> (subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) e. Top)
89	57, 62, 88	syl11anc 524	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) e. Top)
90		df-ima 4007	. . . . . . . . . . . . . . . 16 |- (F"(A[,]B)) = ran ( F |` (A[,]B))
91	90	sseq1i 2641	. . . . . . . . . . . . . . 15 |- ((F"(A[,]B)) C_ RR <-> ran ( F |` (A[,]B)) C_ RR)
92	91	biimpi 168	. . . . . . . . . . . . . 14 |- ((F"(A[,]B)) C_ RR -> ran ( F |` (A[,]B)) C_ RR)
93	92	3ad2ant2 898	. . . . . . . . . . . . 13 |- ((F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))) -> ran ( F |` (A[,]B)) C_ RR)
94	93	3ad2ant3 899	. . . . . . . . . . . 12 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> ran ( F |` (A[,]B)) C_ RR)
95	94	3ad2ant3 899	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ran ( F |` (A[,]B)) C_ RR)
96		axresscn 6420	. . . . . . . . . . . 12 |- RR C_ CC
97	96	a1i 8	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> RR C_ CC)
98	54	eqcomi 1888	. . . . . . . . . . . 12 |- CC = U.(Open` (abs o. - ))
99	98	cnsubsp2 15427	. . . . . . . . . . 11 |- ((((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) e. Top /\ (Open` (abs o. - )) e. Top) /\ (ran ( F |` (A[,]B)) C_ RR /\ RR C_ CC)) -> ((F |` (A[,]B)) e. ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (Open` (abs o. - ))) <-> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (subSp` <.RR, (Open` (abs o. - ))>.))))
100	89, 49, 95, 97, 99	syl22anc 1101	. . . . . . . . . 10 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((F |` (A[,]B)) e. ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (Open` (abs o. - ))) <-> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (subSp` <.RR, (Open` (abs o. - ))>.))))
101	87, 100	mpbid 212	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (subSp` <.RR, (Open` (abs o. - ))>.)))
102	98	subsubtop 15423	. . . . . . . . . . . . . 14 |- (((Open` (abs o. - )) e. Top /\ (A[,]B) C_ D /\ D C_ CC) -> (subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) = (subSp` <.(A[,]B), (Open` (abs o. - ))>.))
103	49, 59, 51, 102	syl111anc 1100	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) = (subSp` <.(A[,]B), (Open` (abs o. - ))>.))
104	98	subsubtop 15423	. . . . . . . . . . . . . 14 |- (((Open` (abs o. - )) e. Top /\ (A[,]B) C_ RR /\ RR C_ CC) -> (subSp` <.(A[,]B), (subSp` <.RR, (Open` (abs o. - ))>.)>.) = (subSp` <.(A[,]B), (Open` (abs o. - ))>.))
105	49, 32, 97, 104	syl111anc 1100	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(A[,]B), (subSp` <.RR, (Open` (abs o. - ))>.)>.) = (subSp` <.(A[,]B), (Open` (abs o. - ))>.))
106	103, 105	eqtr4d 1928	. . . . . . . . . . . 12 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) = (subSp` <.(A[,]B), (subSp` <.RR, (Open` (abs o. - ))>.)>.))
107		eqid 1884	. . . . . . . . . . . . . . 15 |- ((abs o. - ) |` (RR X. RR)) = ((abs o. - ) |` (RR X. RR))
108		eqid 1884	. . . . . . . . . . . . . . . . 17 |- (Open` ((abs o. - ) |` (RR X. RR))) = (Open` ((abs o. - ) |` (RR X. RR)))
109	107, 52, 46, 108	subtopmet 10256	. . . . . . . . . . . . . . . 16 |- (((abs o. - ) e. Met /\ RR C_ CC) -> (subSp` <.RR, (Open` (abs o. - ))>.) = (Open` ((abs o. - ) |` (RR X. RR))))
110	45, 96, 109	mp2an 761	. . . . . . . . . . . . . . 15 |- (subSp` <.RR, (Open` (abs o. - ))>.) = (Open` ((abs o. - ) |` (RR X. RR)))
111	107, 110	tgioo 9193	. . . . . . . . . . . . . 14 |- (topGen` ran (,)) = (subSp` <.RR, (Open` (abs o. - ))>.)
112	111	opeq2i 3162	. . . . . . . . . . . . 13 |- <.(A[,]B), (topGen` ran (,))>. = <.(A[,]B), (subSp` <.RR, (Open` (abs o. - ))>.)>.
113	112	fveq2i 4684	. . . . . . . . . . . 12 |- (subSp` <.(A[,]B), (topGen` ran (,))>.) = (subSp` <.(A[,]B), (subSp` <.RR, (Open` (abs o. - ))>.)>.)
114	106, 113	syl6eqr 1946	. . . . . . . . . . 11 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) = (subSp` <.(A[,]B), (topGen` ran (,))>.))
115	114	opreq1d 4897	. . . . . . . . . 10 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (subSp` <.RR, (Open` (abs o. - ))>.)) = ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (subSp` <.RR, (Open` (abs o. - ))>.)))
116	107, 108	tgioo 9193	. . . . . . . . . . . 12 |- (topGen` ran (,)) = (Open` ((abs o. - ) |` (RR X. RR)))
117	110, 116	eqtr4i 1911	. . . . . . . . . . 11 |- (subSp` <.RR, (Open` (abs o. - ))>.) = (topGen` ran (,))
118	117	opreq2i 4893	. . . . . . . . . 10 |- ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (subSp` <.RR, (Open` (abs o. - ))>.)) = ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (topGen` ran (,)))
119	115, 118	syl6eq 1944	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((subSp` <.(A[,]B), (subSp` <.D, (Open` (abs o. - ))>.)>.) Cn (subSp` <.RR, (Open` (abs o. - ))>.)) = ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (topGen` ran (,))))
120	101, 119	eleqtrd 1973	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (topGen` ran (,))))
121		stoig3 10253	. . . . . . . . . . 11 |- (((topGen` ran (,)) e. Top /\ (A[,]B) C_ U.(topGen` ran (,))) -> (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Top)
122	12, 121	mpan 759	. . . . . . . . . 10 |- ((A[,]B) C_ U.(topGen` ran (,)) -> (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Top)
123	33, 122	syl 12	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(A[,]B), (topGen` ran (,))>.) e. Top)
124	90	eqimss2i 2669	. . . . . . . . . 10 |- ran ( F |` (A[,]B)) C_ (F"(A[,]B))
125	124	a1i 8	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ran ( F |` (A[,]B)) C_ (F"(A[,]B)))
126	15	eqcomi 1888	. . . . . . . . . 10 |- RR = U.(topGen` ran (,))
127	126	cnsubsp2 15427	. . . . . . . . 9 |- ((((subSp` <.(A[,]B), (topGen` ran (,))>.) e. Top /\ (topGen` ran (,)) e. Top) /\ (ran ( F |` (A[,]B)) C_ (F"(A[,]B)) /\ (F"(A[,]B)) C_ RR)) -> ((F |` (A[,]B)) e. ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (topGen` ran (,))) <-> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.))))
128	123, 13, 125, 14, 127	syl22anc 1101	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((F |` (A[,]B)) e. ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (topGen` ran (,))) <-> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.))))
129	120, 128	mpbid 212	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.)))
130		eqid 1884	. . . . . . . 8 |- U.(subSp` <.(A[,]B), (topGen` ran (,))>.) = U.(subSp` <.(A[,]B), (topGen` ran (,))>.)
131		eqid 1884	. . . . . . . 8 |- U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) = U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.)
132	130, 131	cnconn 15444	. . . . . . 7 |- ((((subSp` <.(A[,]B), (topGen` ran (,))>.) e. Con /\ (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Top) /\ ((F |` (A[,]B)):U.(subSp` <.(A[,]B), (topGen` ran (,))>.)-onto->U.(subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) /\ (F |` (A[,]B)) e. ((subSp` <.(A[,]B), (topGen` ran (,))>.) Cn (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.)))) -> (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Con)
133	11, 18, 43, 129, 132	syl22anc 1101	. . . . . 6 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Con)
134		reconn 15451	. . . . . . . . 9 |- ((F"(A[,]B)) C_ RR -> ((subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Con <-> A.x e. (F"(A[,]B))A.y e. (F"(A[,]B))(x[,]y) C_ (F"(A[,]B))))
135	134	3ad2ant2 898	. . . . . . . 8 |- ((F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))) -> ((subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Con <-> A.x e. (F"(A[,]B))A.y e. (F"(A[,]B))(x[,]y) C_ (F"(A[,]B))))
136	135	3ad2ant3 899	. . . . . . 7 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> ((subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Con <-> A.x e. (F"(A[,]B))A.y e. (F"(A[,]B))(x[,]y) C_ (F"(A[,]B))))
137	136	3ad2ant3 899	. . . . . 6 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((subSp` <.(F"(A[,]B)), (topGen` ran (,))>.) e. Con <-> A.x e. (F"(A[,]B))A.y e. (F"(A[,]B))(x[,]y) C_ (F"(A[,]B))))
138	133, 137	mpbid 212	. . . . 5 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> A.x e. (F"(A[,]B))A.y e. (F"(A[,]B))(x[,]y) C_ (F"(A[,]B)))
139	22, 27	syl 12	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (Fun F /\ (A[,]B) C_ dom F))
140		simp1 876	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ U e. RR) -> A e. RR)
141	140	3ad2ant1 897	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> A e. RR)
142		simp2 877	. . . . . . . . 9 |- ((A e. RR /\ B e. RR /\ U e. RR) -> B e. RR)
143	142	3ad2ant1 897	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> B e. RR)
144		ltle 6690	. . . . . . . . . . 11 |- ((A e. RR /\ B e. RR) -> (A < B -> A <_ B))
145	144	imp 377	. . . . . . . . . 10 |- (((A e. RR /\ B e. RR) /\ A < B) -> A <_ B)
146	145	3adantl3 1034	. . . . . . . . 9 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B) -> A <_ B)
147	146	3adant3 896	. . . . . . . 8 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> A <_ B)
148		lbicc2 7573	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A <_ B) -> A e. (A[,]B))
149	141, 143, 147, 148	syl111anc 1100	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> A e. (A[,]B))
150		funfvima2 4829	. . . . . . 7 |- ((Fun F /\ (A[,]B) C_ dom F) -> (A e. (A[,]B) -> (F` A) e. (F"(A[,]B))))
151	139, 149, 150	sylc 83	. . . . . 6 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` A) e. (F"(A[,]B)))
152		ubicc2 7574	. . . . . . . 8 |- ((A e. RR /\ B e. RR /\ A <_ B) -> B e. (A[,]B))
153	141, 143, 147, 152	syl111anc 1100	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> B e. (A[,]B))
154		funfvima2 4829	. . . . . . 7 |- ((Fun F /\ (A[,]B) C_ dom F) -> (B e. (A[,]B) -> (F` B) e. (F"(A[,]B))))
155	139, 153, 154	sylc 83	. . . . . 6 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` B) e. (F"(A[,]B)))
156		opreq1 4889	. . . . . . . 8 |- (x = (F` A) -> (x[,]y) = ((F` A)[,]y))
157	156	sseq1d 2644	. . . . . . 7 |- (x = (F` A) -> ((x[,]y) C_ (F"(A[,]B)) <-> ((F` A)[,]y) C_ (F"(A[,]B))))
158		opreq2 4890	. . . . . . . 8 |- (y = (F` B) -> ((F` A)[,]y) = ((F` A)[,](F` B)))
159	158	sseq1d 2644	. . . . . . 7 |- (y = (F` B) -> (((F` A)[,]y) C_ (F"(A[,]B)) <-> ((F` A)[,](F` B)) C_ (F"(A[,]B))))
160	157, 159	rcla42v 2384	. . . . . 6 |- (((F` A) e. (F"(A[,]B)) /\ (F` B) e. (F"(A[,]B))) -> (A.x e. (F"(A[,]B))A.y e. (F"(A[,]B))(x[,]y) C_ (F"(A[,]B)) -> ((F` A)[,](F` B)) C_ (F"(A[,]B))))
161	151, 155, 160	syl11anc 524	. . . . 5 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (A.x e. (F"(A[,]B))A.y e. (F"(A[,]B))(x[,]y) C_ (F"(A[,]B)) -> ((F` A)[,](F` B)) C_ (F"(A[,]B))))
162	138, 161	mpd 29	. . . 4 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((F` A)[,](F` B)) C_ (F"(A[,]B)))
163		ioossicc 7566	. . . . . . . 8 |- ((F` A)(,)(F` B)) C_ ((F` A)[,](F` B))
164	163	sseli 2617	. . . . . . 7 |- (U e. ((F` A)(,)(F` B)) -> U e. ((F` A)[,](F` B)))
165	164	3ad2ant3 899	. . . . . 6 |- ((F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))) -> U e. ((F` A)[,](F` B)))
166	165	3ad2ant3 899	. . . . 5 |- (((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B)))) -> U e. ((F` A)[,](F` B)))
167	166	3ad2ant3 899	. . . 4 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U e. ((F` A)[,](F` B)))
168	162, 167	sseldd 2620	. . 3 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U e. (F"(A[,]B)))
169		fvelima 4723	. . 3 |- ((Fun F /\ U e. (F"(A[,]B))) -> E.x e. (A[,]B)(F` x) = U)
170	8, 168, 169	syl11anc 524	. 2 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> E.x e. (A[,]B)(F` x) = U)
171		simp1 876	. . . . . . . . 9 |- ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) -> x e. RR*)
172	171	adantr 425	. . . . . . . 8 |- (((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U) -> x e. RR*)
173	172	a1i 8	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U) -> x e. RR*))
174	14, 151	sseldd 2620	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` A) e. RR)
175		simp3 878	. . . . . . . . . . . . . . 15 |- ((A e. RR /\ B e. RR /\ U e. RR) -> U e. RR)
176	175	3ad2ant1 897	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U e. RR)
177		simp333 1031	. . . . . . . . . . . . . . . 16 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U e. ((F` A)(,)(F` B)))
178		rexr 6668	. . . . . . . . . . . . . . . . . 18 |- ((F` A) e. RR -> (F` A) e. RR*)
179	174, 178	syl 12	. . . . . . . . . . . . . . . . 17 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` A) e. RR*)
180	14, 155	sseldd 2620	. . . . . . . . . . . . . . . . . 18 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` B) e. RR)
181		rexr 6668	. . . . . . . . . . . . . . . . . 18 |- ((F` B) e. RR -> (F` B) e. RR*)
182	180, 181	syl 12	. . . . . . . . . . . . . . . . 17 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` B) e. RR*)
183		elioo2 7546	. . . . . . . . . . . . . . . . 17 |- (((F` A) e. RR* /\ (F` B) e. RR*) -> (U e. ((F` A)(,)(F` B)) <-> (U e. RR /\ (F` A) < U /\ U < (F` B))))
184	179, 182, 183	syl11anc 524	. . . . . . . . . . . . . . . 16 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (U e. ((F` A)(,)(F` B)) <-> (U e. RR /\ (F` A) < U /\ U < (F` B))))
185	177, 184	mpbid 212	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (U e. RR /\ (F` A) < U /\ U < (F` B)))
186	185	simp2d 889	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` A) < U)
187		ltne 6686	. . . . . . . . . . . . . 14 |- (((F` A) e. RR /\ U e. RR /\ (F` A) < U) -> U =/= (F` A))
188	174, 176, 186, 187	syl111anc 1100	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U =/= (F` A))
189	188	adantr 425	. . . . . . . . . . . 12 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> U =/= (F` A))
190		simprr 451	. . . . . . . . . . . . 13 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> (F` x) = U)
191	190	neeq1d 2028	. . . . . . . . . . . 12 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> ((F` x) =/= (F` A) <-> U =/= (F` A)))
192	189, 191	mpbird 213	. . . . . . . . . . 11 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> (F` x) =/= (F` A))
193		df-ne 2019	. . . . . . . . . . 11 |- ((F` x) =/= (F` A) <-> -. (F` x) = (F` A))
194	192, 193	sylib 215	. . . . . . . . . 10 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> -. (F` x) = (F` A))
195		fveq2 4681	. . . . . . . . . 10 |- (x = A -> (F` x) = (F` A))
196	194, 195	nsyl 131	. . . . . . . . 9 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> -. x = A)
197	185	simp3d 890	. . . . . . . . . . . . . . 15 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U < (F` B))
198		ltne 6686	. . . . . . . . . . . . . . 15 |- ((U e. RR /\ (F` B) e. RR /\ U < (F` B)) -> (F` B) =/= U)
199	176, 180, 197, 198	syl111anc 1100	. . . . . . . . . . . . . 14 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (F` B) =/= U)
200	199	necomd 2095	. . . . . . . . . . . . 13 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> U =/= (F` B))
201	200	adantr 425	. . . . . . . . . . . 12 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> U =/= (F` B))
202	190	neeq1d 2028	. . . . . . . . . . . 12 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> ((F` x) =/= (F` B) <-> U =/= (F` B)))
203	201, 202	mpbird 213	. . . . . . . . . . 11 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> (F` x) =/= (F` B))
204		df-ne 2019	. . . . . . . . . . 11 |- ((F` x) =/= (F` B) <-> -. (F` x) = (F` B))
205	203, 204	sylib 215	. . . . . . . . . 10 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> -. (F` x) = (F` B))
206		fveq2 4681	. . . . . . . . . 10 |- (x = B -> (F` x) = (F` B))
207	205, 206	nsyl 131	. . . . . . . . 9 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> -. x = B)
208		simprl3 923	. . . . . . . . 9 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> (x = A \/ (A < x /\ x < B) \/ x = B))
209	196, 207, 208	ecase13d 15350	. . . . . . . 8 |- ((((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) /\ ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)) -> (A < x /\ x < B))
210	209	ex 402	. . . . . . 7 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U) -> (A < x /\ x < B)))
211	173, 210	jcad 661	. . . . . 6 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U) -> (x e. RR* /\ (A < x /\ x < B))))
212		3anass 862	. . . . . 6 |- ((x e. RR* /\ A < x /\ x < B) <-> (x e. RR* /\ (A < x /\ x < B)))
213	211, 212	syl6ibr 230	. . . . 5 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U) -> (x e. RR* /\ A < x /\ x < B)))
214		elicc3 15362	. . . . . . . . 9 |- ((A e. RR* /\ B e. RR*) -> (x e. (A[,]B) <-> (x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B))))
215		rexr 6668	. . . . . . . . 9 |- (A e. RR -> A e. RR*)
216		rexr 6668	. . . . . . . . 9 |- (B e. RR -> B e. RR*)
217	214, 215, 216	syl2an 503	. . . . . . . 8 |- ((A e. RR /\ B e. RR) -> (x e. (A[,]B) <-> (x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B))))
218	217	3adant3 896	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ U e. RR) -> (x e. (A[,]B) <-> (x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B))))
219	218	3ad2ant1 897	. . . . . 6 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (x e. (A[,]B) <-> (x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B))))
220	219	anbi1d 679	. . . . 5 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((x e. (A[,]B) /\ (F` x) = U) <-> ((x e. RR* /\ A <_ B /\ (x = A \/ (A < x /\ x < B) \/ x = B)) /\ (F` x) = U)))
221		elioo1 7545	. . . . . . . 8 |- ((A e. RR* /\ B e. RR*) -> (x e. (A(,)B) <-> (x e. RR* /\ A < x /\ x < B)))
222	221, 215, 216	syl2an 503	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> (x e. (A(,)B) <-> (x e. RR* /\ A < x /\ x < B)))
223	222	3adant3 896	. . . . . 6 |- ((A e. RR /\ B e. RR /\ U e. RR) -> (x e. (A(,)B) <-> (x e. RR* /\ A < x /\ x < B)))
224	223	3ad2ant1 897	. . . . 5 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (x e. (A(,)B) <-> (x e. RR* /\ A < x /\ x < B)))
225	213, 220, 224	3imtr4d 602	. . . 4 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((x e. (A[,]B) /\ (F` x) = U) -> x e. (A(,)B)))
226		simpr 350	. . . . 5 |- ((x e. (A[,]B) /\ (F` x) = U) -> (F` x) = U)
227	226	a1i 8	. . . 4 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((x e. (A[,]B) /\ (F` x) = U) -> (F` x) = U))
228	225, 227	jcad 661	. . 3 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> ((x e. (A[,]B) /\ (F` x) = U) -> (x e. (A(,)B) /\ (F` x) = U)))
229	228	reximdv2 2200	. 2 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> (E.x e. (A[,]B)(F` x) = U -> E.x e. (A(,)B)(F` x) = U))
230	170, 229	mpd 29	1 |- (((A e. RR /\ B e. RR /\ U e. RR) /\ A < B /\ ((A[,]B) C_ D /\ D C_ CC /\ (F e. (D-cn->CC) /\ (F"(A[,]B)) C_ RR /\ U e. ((F` A)(,)(F` B))))) -> E.x e. (A(,)B)(F` x) = U)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   C_ wss 2593  <.cop 3046  U.cuni 3177   class class class wbr 3338   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988  "cima 3989   o. ccom 3990  Rel wrel 3991  Fun wfun 3992  -->wf 3994  -onto->wfo 3996  ` cfv 3998  (class class class)co 4884  CCcc 6384  RRcr 6385   - cmin 6445   <_ cle 6448  RR*cxr 6652   < clt 6653  (,)cioo 7524  [,]cicc 7527  abscabs 8000  -cn->ccncf 8524  Topctop 8857  topGenctg 8860   Cn ccn 9028  Metcme 9066  Opencopn 9069  subSpcsubsp 10242  Conccon 10337

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-map 5383  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-sup 5664  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-div 6892  df-n 7108  df-2 7154  df-rp 7232  df-n0 7309  df-z 7345  df-q 7436  df-ioo 7528  df-icc 7531  df-seq1 7721  df-exp 7812  df-sqr 7920  df-re 8001  df-im 8002  df-cj 8003  df-abs 8004  df-cncf 8525  df-top 8861  df-topsp 8862  df-bases 8863  df-topgen 8864  df-cld 8939  df-cn 9030  df-cnp 9031  df-met 9070  df-bl 9072  df-opn 9073  df-subsp 10243  df-con 10338

Copyright terms: Public domain