isr0

Description: The property " J is an R_0 space". A space is R_0 if any two topologically distinguishable points are separated (there is an open set containing each one and disjoint from the other). Or in contraposition, if every open set which contains x also contains y , so there is no separation, then x and y are members of the same open sets. We have chosen not to give this definition a name, because it turns out that a space is R_0 if and only if its Kolmogorov quotient is T_1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	kqval.2	\|- F = ( x e. X \|-> { y e. J \| x e. y } )
	Assertion	isr0	\|- ( J e. ( TopOn ` X ) -> ( ( KQ ` J ) e. Fre <-> A. z e. X A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		kqval.2	\|- F = ( x e. X \|-> { y e. J \| x e. y } )
2	1	kqid	\|- ( J e. ( TopOn ` X ) -> F e. ( J Cn ( KQ ` J ) ) )
3	2	ad2antrr	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> F e. ( J Cn ( KQ ` J ) ) )
4		cnima	\|- ( ( F e. ( J Cn ( KQ ` J ) ) /\ v e. ( KQ ` J ) ) -> ( `' F " v ) e. J )
5	3 4	sylan	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> ( `' F " v ) e. J )
6		eleq2	\|- ( o = ( `' F " v ) -> ( z e. o <-> z e. ( `' F " v ) ) )
7		eleq2	\|- ( o = ( `' F " v ) -> ( w e. o <-> w e. ( `' F " v ) ) )
8	6 7	imbi12d	\|- ( o = ( `' F " v ) -> ( ( z e. o -> w e. o ) <-> ( z e. ( `' F " v ) -> w e. ( `' F " v ) ) ) )
9	8	rspcv	\|- ( ( `' F " v ) e. J -> ( A. o e. J ( z e. o -> w e. o ) -> ( z e. ( `' F " v ) -> w e. ( `' F " v ) ) ) )
10	5 9	syl	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> ( A. o e. J ( z e. o -> w e. o ) -> ( z e. ( `' F " v ) -> w e. ( `' F " v ) ) ) )
11	1	kqffn	\|- ( J e. ( TopOn ` X ) -> F Fn X )
12	11	ad2antrr	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> F Fn X )
13	12	adantr	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> F Fn X )
14		fnfun	\|- ( F Fn X -> Fun F )
15	13 14	syl	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> Fun F )
16		simprl	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> z e. X )
17	16	adantr	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> z e. X )
18	13	fndmd	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> dom F = X )
19	17 18	eleqtrrd	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> z e. dom F )
20		fvimacnv	\|- ( ( Fun F /\ z e. dom F ) -> ( ( F ` z ) e. v <-> z e. ( `' F " v ) ) )
21	15 19 20	syl2anc	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> ( ( F ` z ) e. v <-> z e. ( `' F " v ) ) )
22		simprr	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> w e. X )
23	22	adantr	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> w e. X )
24	23 18	eleqtrrd	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> w e. dom F )
25		fvimacnv	\|- ( ( Fun F /\ w e. dom F ) -> ( ( F ` w ) e. v <-> w e. ( `' F " v ) ) )
26	15 24 25	syl2anc	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> ( ( F ` w ) e. v <-> w e. ( `' F " v ) ) )
27	21 26	imbi12d	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> ( ( ( F ` z ) e. v -> ( F ` w ) e. v ) <-> ( z e. ( `' F " v ) -> w e. ( `' F " v ) ) ) )
28	10 27	sylibrd	\|- ( ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) /\ v e. ( KQ ` J ) ) -> ( A. o e. J ( z e. o -> w e. o ) -> ( ( F ` z ) e. v -> ( F ` w ) e. v ) ) )
29	28	ralrimdva	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( A. o e. J ( z e. o -> w e. o ) -> A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) ) )
30		simplr	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( KQ ` J ) e. Fre )
31		fnfvelrn	\|- ( ( F Fn X /\ z e. X ) -> ( F ` z ) e. ran F )
32	12 16 31	syl2anc	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) e. ran F )
33	1	kqtopon	\|- ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
34	33	ad2antrr	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
35		toponuni	\|- ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ran F = U. ( KQ ` J ) )
36	34 35	syl	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ran F = U. ( KQ ` J ) )
37	32 36	eleqtrd	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` z ) e. U. ( KQ ` J ) )
38		fnfvelrn	\|- ( ( F Fn X /\ w e. X ) -> ( F ` w ) e. ran F )
39	12 22 38	syl2anc	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` w ) e. ran F )
40	39 36	eleqtrd	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( F ` w ) e. U. ( KQ ` J ) )
41		eqid	\|- U. ( KQ ` J ) = U. ( KQ ` J )
42	41	t1sep2	\|- ( ( ( KQ ` J ) e. Fre /\ ( F ` z ) e. U. ( KQ ` J ) /\ ( F ` w ) e. U. ( KQ ` J ) ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) )
43	30 37 40 42	syl3anc	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) )
44	29 43	syld	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( A. o e. J ( z e. o -> w e. o ) -> ( F ` z ) = ( F ` w ) ) )
45	1	kqfeq	\|- ( ( J e. ( TopOn ` X ) /\ z e. X /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. y e. J ( z e. y <-> w e. y ) ) )
46		eleq2	\|- ( o = y -> ( z e. o <-> z e. y ) )
47		eleq2	\|- ( o = y -> ( w e. o <-> w e. y ) )
48	46 47	bibi12d	\|- ( o = y -> ( ( z e. o <-> w e. o ) <-> ( z e. y <-> w e. y ) ) )
49	48	cbvralvw	\|- ( A. o e. J ( z e. o <-> w e. o ) <-> A. y e. J ( z e. y <-> w e. y ) )
50	45 49	bitr4di	\|- ( ( J e. ( TopOn ` X ) /\ z e. X /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. o e. J ( z e. o <-> w e. o ) ) )
51	50	3expb	\|- ( ( J e. ( TopOn ` X ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) = ( F ` w ) <-> A. o e. J ( z e. o <-> w e. o ) ) )
52	51	adantlr	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( ( F ` z ) = ( F ` w ) <-> A. o e. J ( z e. o <-> w e. o ) ) )
53	44 52	sylibd	\|- ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) /\ ( z e. X /\ w e. X ) ) -> ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) )
54	53	ralrimivva	\|- ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre ) -> A. z e. X A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) )
55	54	ex	\|- ( J e. ( TopOn ` X ) -> ( ( KQ ` J ) e. Fre -> A. z e. X A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) ) )
56	1	kqopn	\|- ( ( J e. ( TopOn ` X ) /\ o e. J ) -> ( F " o ) e. ( KQ ` J ) )
57	56	ad4ant14	\|- ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( F " o ) e. ( KQ ` J ) )
58		eleq2	\|- ( v = ( F " o ) -> ( ( F ` z ) e. v <-> ( F ` z ) e. ( F " o ) ) )
59		eleq2	\|- ( v = ( F " o ) -> ( ( F ` w ) e. v <-> ( F ` w ) e. ( F " o ) ) )
60	58 59	imbi12d	\|- ( v = ( F " o ) -> ( ( ( F ` z ) e. v -> ( F ` w ) e. v ) <-> ( ( F ` z ) e. ( F " o ) -> ( F ` w ) e. ( F " o ) ) ) )
61	60	rspcv	\|- ( ( F " o ) e. ( KQ ` J ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( ( F ` z ) e. ( F " o ) -> ( F ` w ) e. ( F " o ) ) ) )
62	57 61	syl	\|- ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( ( F ` z ) e. ( F " o ) -> ( F ` w ) e. ( F " o ) ) ) )
63	1	kqfvima	\|- ( ( J e. ( TopOn ` X ) /\ o e. J /\ z e. X ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
64	63	3expa	\|- ( ( ( J e. ( TopOn ` X ) /\ o e. J ) /\ z e. X ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
65	64	an32s	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ o e. J ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
66	65	adantlr	\|- ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( z e. o <-> ( F ` z ) e. ( F " o ) ) )
67	1	kqfvima	\|- ( ( J e. ( TopOn ` X ) /\ o e. J /\ w e. X ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
68	67	3expa	\|- ( ( ( J e. ( TopOn ` X ) /\ o e. J ) /\ w e. X ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
69	68	an32s	\|- ( ( ( J e. ( TopOn ` X ) /\ w e. X ) /\ o e. J ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
70	69	adantllr	\|- ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( w e. o <-> ( F ` w ) e. ( F " o ) ) )
71	66 70	imbi12d	\|- ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( ( z e. o -> w e. o ) <-> ( ( F ` z ) e. ( F " o ) -> ( F ` w ) e. ( F " o ) ) ) )
72	62 71	sylibrd	\|- ( ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) /\ o e. J ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( z e. o -> w e. o ) ) )
73	72	ralrimdva	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> A. o e. J ( z e. o -> w e. o ) ) )
74	1	kqfval	\|- ( ( J e. ( TopOn ` X ) /\ z e. X ) -> ( F ` z ) = { y e. J \| z e. y } )
75	74	adantr	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( F ` z ) = { y e. J \| z e. y } )
76	1	kqfval	\|- ( ( J e. ( TopOn ` X ) /\ w e. X ) -> ( F ` w ) = { y e. J \| w e. y } )
77	76	adantlr	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( F ` w ) = { y e. J \| w e. y } )
78	75 77	eqeq12d	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> { y e. J \| z e. y } = { y e. J \| w e. y } ) )
79		rabbi	\|- ( A. y e. J ( z e. y <-> w e. y ) <-> { y e. J \| z e. y } = { y e. J \| w e. y } )
80	49 79	bitri	\|- ( A. o e. J ( z e. o <-> w e. o ) <-> { y e. J \| z e. y } = { y e. J \| w e. y } )
81	78 80	bitr4di	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( ( F ` z ) = ( F ` w ) <-> A. o e. J ( z e. o <-> w e. o ) ) )
82	81	biimprd	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( A. o e. J ( z e. o <-> w e. o ) -> ( F ` z ) = ( F ` w ) ) )
83	73 82	imim12d	\|- ( ( ( J e. ( TopOn ` X ) /\ z e. X ) /\ w e. X ) -> ( ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
84	83	ralimdva	\|- ( ( J e. ( TopOn ` X ) /\ z e. X ) -> ( A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) -> A. w e. X ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
85	84	ralimdva	\|- ( J e. ( TopOn ` X ) -> ( A. z e. X A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) -> A. z e. X A. w e. X ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
86		eleq1	\|- ( a = ( F ` z ) -> ( a e. v <-> ( F ` z ) e. v ) )
87	86	imbi1d	\|- ( a = ( F ` z ) -> ( ( a e. v -> b e. v ) <-> ( ( F ` z ) e. v -> b e. v ) ) )
88	87	ralbidv	\|- ( a = ( F ` z ) -> ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) <-> A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) ) )
89		eqeq1	\|- ( a = ( F ` z ) -> ( a = b <-> ( F ` z ) = b ) )
90	88 89	imbi12d	\|- ( a = ( F ` z ) -> ( ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) <-> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) -> ( F ` z ) = b ) ) )
91	90	ralbidv	\|- ( a = ( F ` z ) -> ( A. b e. ran F ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) <-> A. b e. ran F ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) -> ( F ` z ) = b ) ) )
92	91	ralrn	\|- ( F Fn X -> ( A. a e. ran F A. b e. ran F ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) <-> A. z e. X A. b e. ran F ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) -> ( F ` z ) = b ) ) )
93		eleq1	\|- ( b = ( F ` w ) -> ( b e. v <-> ( F ` w ) e. v ) )
94	93	imbi2d	\|- ( b = ( F ` w ) -> ( ( ( F ` z ) e. v -> b e. v ) <-> ( ( F ` z ) e. v -> ( F ` w ) e. v ) ) )
95	94	ralbidv	\|- ( b = ( F ` w ) -> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) <-> A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) ) )
96		eqeq2	\|- ( b = ( F ` w ) -> ( ( F ` z ) = b <-> ( F ` z ) = ( F ` w ) ) )
97	95 96	imbi12d	\|- ( b = ( F ` w ) -> ( ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) -> ( F ` z ) = b ) <-> ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
98	97	ralrn	\|- ( F Fn X -> ( A. b e. ran F ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) -> ( F ` z ) = b ) <-> A. w e. X ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
99	98	ralbidv	\|- ( F Fn X -> ( A. z e. X A. b e. ran F ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> b e. v ) -> ( F ` z ) = b ) <-> A. z e. X A. w e. X ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
100	92 99	bitrd	\|- ( F Fn X -> ( A. a e. ran F A. b e. ran F ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) <-> A. z e. X A. w e. X ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
101	11 100	syl	\|- ( J e. ( TopOn ` X ) -> ( A. a e. ran F A. b e. ran F ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) <-> A. z e. X A. w e. X ( A. v e. ( KQ ` J ) ( ( F ` z ) e. v -> ( F ` w ) e. v ) -> ( F ` z ) = ( F ` w ) ) ) )
102	85 101	sylibrd	\|- ( J e. ( TopOn ` X ) -> ( A. z e. X A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) -> A. a e. ran F A. b e. ran F ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) ) )
103		ist1-2	\|- ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ( ( KQ ` J ) e. Fre <-> A. a e. ran F A. b e. ran F ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) ) )
104	33 103	syl	\|- ( J e. ( TopOn ` X ) -> ( ( KQ ` J ) e. Fre <-> A. a e. ran F A. b e. ran F ( A. v e. ( KQ ` J ) ( a e. v -> b e. v ) -> a = b ) ) )
105	102 104	sylibrd	\|- ( J e. ( TopOn ` X ) -> ( A. z e. X A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) -> ( KQ ` J ) e. Fre ) )
106	55 105	impbid	\|- ( J e. ( TopOn ` X ) -> ( ( KQ ` J ) e. Fre <-> A. z e. X A. w e. X ( A. o e. J ( z e. o -> w e. o ) -> A. o e. J ( z e. o <-> w e. o ) ) ) )

Metamath Proof Explorer

Theorem isr0

Proof