Theorem isnrm2 16637

Description: An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma.

Assertion

Ref	Expression
isnrm2	|- (J e. Top -> (J e. Nrm <-> A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J (c C_ o /\ (((cls` J)` o) i^i d) = (/)))))

Distinct variable group:   c,d,o,J

Proof of Theorem isnrm2

Step	Hyp	Ref	Expression
1		isnrm 16636	. . 3 |- (J e. Nrm <-> (J e. Top /\ A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)))))
2	1	baib 1051	. 2 |- (J e. Top -> (J e. Nrm <-> A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)))))
3		simprr1 1196	. . . . . . . . . . . 12 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> c C_ o)
4		incom 3032	. . . . . . . . . . . . 13 |- (((cls` J)` o) i^i d) = (d i^i ((cls` J)` o))
5		simprr2 1197	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> d C_ p)
6		simplll 871	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> J e. Top)
7		difss 2986	. . . . . . . . . . . . . . . . . 18 |- (U.J \ o) C_ U.J
8	7	a1i 8	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> (U.J \ o) C_ U.J)
9		simprlr 876	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> p e. J)
10		incom 3032	. . . . . . . . . . . . . . . . . . . . . 22 |- (o i^i p) = (p i^i o)
11	10	eqeq1i 2177	. . . . . . . . . . . . . . . . . . . . 21 |- ((o i^i p) = (/) <-> (p i^i o) = (/))
12	11	biimpi 236	. . . . . . . . . . . . . . . . . . . 20 |- ((o i^i p) = (/) -> (p i^i o) = (/))
13	12	3ad2ant3 1171	. . . . . . . . . . . . . . . . . . 19 |- ((c C_ o /\ d C_ p /\ (o i^i p) = (/)) -> (p i^i o) = (/))
14	13	ad2antll 862	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> (p i^i o) = (/))
15		eqid 2170	. . . . . . . . . . . . . . . . . . . . . 22 |- U.J = U.J
16	15	eltopss 9859	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ p e. J) -> p C_ U.J)
17	16	ad2ant2rl 866	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ c e. (Clsd` J)) /\ (o e. J /\ p e. J)) -> p C_ U.J)
18	17	ad2ant2r 864	. . . . . . . . . . . . . . . . . . 19 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> p C_ U.J)
19		reldisj 3153	. . . . . . . . . . . . . . . . . . 19 |- (p C_ U.J -> ((p i^i o) = (/) <-> p C_ (U.J \ o)))
20	18, 19	syl 13	. . . . . . . . . . . . . . . . . 18 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> ((p i^i o) = (/) <-> p C_ (U.J \ o)))
21	14, 20	mpbid 256	. . . . . . . . . . . . . . . . 17 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> p C_ (U.J \ o))
22	15	ssntr 16490	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ (U.J \ o) C_ U.J) /\ (p e. J /\ p C_ (U.J \ o))) -> p C_ ((int` J)` (U.J \ o)))
23	6, 8, 9, 21, 22	syl22anc 1378	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> p C_ ((int` J)` (U.J \ o)))
24	5, 23	sstrd 2889	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> d C_ ((int` J)` (U.J \ o)))
25	15	eltopss 9859	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ o e. J) -> o C_ U.J)
26	25	ad2ant2r 864	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ c e. (Clsd` J)) /\ (o e. J /\ p e. J)) -> o C_ U.J)
27	26	ad2ant2r 864	. . . . . . . . . . . . . . . 16 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> o C_ U.J)
28	15	ntrcmp 16491	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ o C_ U.J) -> ((int` J)` (U.J \ o)) = (U.J \ ((cls` J)` o)))
29	6, 27, 28	syl11anc 755	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> ((int` J)` (U.J \ o)) = (U.J \ ((cls` J)` o)))
30	24, 29	sseqtrd 2912	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> d C_ (U.J \ ((cls` J)` o)))
31	15	cldss 9958	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ d e. (Clsd` J)) -> d C_ U.J)
32	31	ad2ant2r 864	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) -> d C_ U.J)
33	32	adantr 543	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> d C_ U.J)
34		reldisj 3153	. . . . . . . . . . . . . . 15 |- (d C_ U.J -> ((d i^i ((cls` J)` o)) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
35	33, 34	syl 13	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> ((d i^i ((cls` J)` o)) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
36	30, 35	mpbird 257	. . . . . . . . . . . . 13 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> (d i^i ((cls` J)` o)) = (/))
37	4, 36	syl5eq 2214	. . . . . . . . . . . 12 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> (((cls` J)` o) i^i d) = (/))
38	3, 37	jca 590	. . . . . . . . . . 11 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ ((o e. J /\ p e. J) /\ (c C_ o /\ d C_ p /\ (o i^i p) = (/)))) -> (c C_ o /\ (((cls` J)` o) i^i d) = (/)))
39	38	expr 685	. . . . . . . . . 10 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ p e. J)) -> ((c C_ o /\ d C_ p /\ (o i^i p) = (/)) -> (c C_ o /\ (((cls` J)` o) i^i d) = (/))))
40	39	expr 685	. . . . . . . . 9 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ o e. J) -> (p e. J -> ((c C_ o /\ d C_ p /\ (o i^i p) = (/)) -> (c C_ o /\ (((cls` J)` o) i^i d) = (/)))))
41	40	r19.23adv 2493	. . . . . . . 8 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ o e. J) -> (E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)) -> (c C_ o /\ (((cls` J)` o) i^i d) = (/))))
42		simplll 871	. . . . . . . . . . 11 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> J e. Top)
43	25	adantlr 834	. . . . . . . . . . . 12 |- (((J e. Top /\ c e. (Clsd` J)) /\ o e. J) -> o C_ U.J)
44	43	ad2ant2r 864	. . . . . . . . . . 11 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> o C_ U.J)
45	15	cmclsopn 9983	. . . . . . . . . . 11 |- ((J e. Top /\ o C_ U.J) -> (U.J \ ((cls` J)` o)) e. J)
46	42, 44, 45	syl11anc 755	. . . . . . . . . 10 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> (U.J \ ((cls` J)` o)) e. J)
47		simprrl 877	. . . . . . . . . 10 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> c C_ o)
48	4	eqeq1i 2177	. . . . . . . . . . . . . . 15 |- ((((cls` J)` o) i^i d) = (/) <-> (d i^i ((cls` J)` o)) = (/))
49	31, 34	syl 13	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ d e. (Clsd` J)) -> ((d i^i ((cls` J)` o)) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
50	49	ad2ant2r 864	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) -> ((d i^i ((cls` J)` o)) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
51	50	adantr 543	. . . . . . . . . . . . . . 15 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ c C_ o)) -> ((d i^i ((cls` J)` o)) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
52	48, 51	syl5bb 316	. . . . . . . . . . . . . 14 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ c C_ o)) -> ((((cls` J)` o) i^i d) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
53	52	biimpd 244	. . . . . . . . . . . . 13 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ c C_ o)) -> ((((cls` J)` o) i^i d) = (/) -> d C_ (U.J \ ((cls` J)` o))))
54	53	expr 685	. . . . . . . . . . . 12 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ o e. J) -> (c C_ o -> ((((cls` J)` o) i^i d) = (/) -> d C_ (U.J \ ((cls` J)` o)))))
55	54	imp3a 491	. . . . . . . . . . 11 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ o e. J) -> ((c C_ o /\ (((cls` J)` o) i^i d) = (/)) -> d C_ (U.J \ ((cls` J)` o))))
56	55	impr 688	. . . . . . . . . 10 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> d C_ (U.J \ ((cls` J)` o)))
57	15	sscls 9979	. . . . . . . . . . . . . 14 |- ((J e. Top /\ o C_ U.J) -> o C_ ((cls` J)` o))
58	42, 44, 57	syl11anc 755	. . . . . . . . . . . . 13 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> o C_ ((cls` J)` o))
59		ssrin 3062	. . . . . . . . . . . . 13 |- (o C_ ((cls` J)` o) -> (o i^i (U.J \ ((cls` J)` o))) C_ (((cls` J)` o) i^i (U.J \ ((cls` J)` o))))
60	58, 59	syl 13	. . . . . . . . . . . 12 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> (o i^i (U.J \ ((cls` J)` o))) C_ (((cls` J)` o) i^i (U.J \ ((cls` J)` o))))
61		difdisj 3178	. . . . . . . . . . . 12 |- (((cls` J)` o) i^i (U.J \ ((cls` J)` o))) = (/)
62	60, 61	syl6sseq 2924	. . . . . . . . . . 11 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> (o i^i (U.J \ ((cls` J)` o))) C_ (/))
63		ss0 3141	. . . . . . . . . . 11 |- ((o i^i (U.J \ ((cls` J)` o))) C_ (/) -> (o i^i (U.J \ ((cls` J)` o))) = (/))
64	62, 63	syl 13	. . . . . . . . . 10 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> (o i^i (U.J \ ((cls` J)` o))) = (/))
65		sseq2 2898	. . . . . . . . . . . 12 |- (p = (U.J \ ((cls` J)` o)) -> (d C_ p <-> d C_ (U.J \ ((cls` J)` o))))
66		ineq2 3035	. . . . . . . . . . . . 13 |- (p = (U.J \ ((cls` J)` o)) -> (o i^i p) = (o i^i (U.J \ ((cls` J)` o))))
67	66	eqeq1d 2178	. . . . . . . . . . . 12 |- (p = (U.J \ ((cls` J)` o)) -> ((o i^i p) = (/) <-> (o i^i (U.J \ ((cls` J)` o))) = (/)))
68	65, 67	3anbi23d 1472	. . . . . . . . . . 11 |- (p = (U.J \ ((cls` J)` o)) -> ((c C_ o /\ d C_ p /\ (o i^i p) = (/)) <-> (c C_ o /\ d C_ (U.J \ ((cls` J)` o)) /\ (o i^i (U.J \ ((cls` J)` o))) = (/))))
69	68	rcla4ev 2651	. . . . . . . . . 10 |- (((U.J \ ((cls` J)` o)) e. J /\ (c C_ o /\ d C_ (U.J \ ((cls` J)` o)) /\ (o i^i (U.J \ ((cls` J)` o))) = (/))) -> E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)))
70	46, 47, 56, 64, 69	syl13anc 1379	. . . . . . . . 9 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ (o e. J /\ (c C_ o /\ (((cls` J)` o) i^i d) = (/)))) -> E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)))
71	70	expr 685	. . . . . . . 8 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ o e. J) -> ((c C_ o /\ (((cls` J)` o) i^i d) = (/)) -> E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/))))
72	41, 71	impbid 250	. . . . . . 7 |- ((((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) /\ o e. J) -> (E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)) <-> (c C_ o /\ (((cls` J)` o) i^i d) = (/))))
73	72	rexbidva 2400	. . . . . 6 |- (((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) -> (E.o e. J E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)) <-> E.o e. J (c C_ o /\ (((cls` J)` o) i^i d) = (/))))
74	73	expr 685	. . . . 5 |- (((J e. Top /\ c e. (Clsd` J)) /\ d e. (Clsd` J)) -> ((c i^i d) = (/) -> (E.o e. J E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/)) <-> E.o e. J (c C_ o /\ (((cls` J)` o) i^i d) = (/)))))
75	74	pm5.74d 304	. . . 4 |- (((J e. Top /\ c e. (Clsd` J)) /\ d e. (Clsd` J)) -> (((c i^i d) = (/) -> E.o e. J E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/))) <-> ((c i^i d) = (/) -> E.o e. J (c C_ o /\ (((cls` J)` o) i^i d) = (/)))))
76	75	ralbidva 2399	. . 3 |- ((J e. Top /\ c e. (Clsd` J)) -> (A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/))) <-> A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J (c C_ o /\ (((cls` J)` o) i^i d) = (/)))))
77	76	ralbidva 2399	. 2 |- (J e. Top -> (A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J E.p e. J (c C_ o /\ d C_ p /\ (o i^i p) = (/))) <-> A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J (c C_ o /\ (((cls` J)` o) i^i d) = (/)))))
78	2, 77	bitrd 311	1 |- (J e. Top -> (J e. Nrm <-> A.c e. (Clsd` J)A.d e. (Clsd` J)((c i^i d) = (/) -> E.o e. J (c C_ o /\ (((cls` J)` o) i^i d) = (/)))))

Syntax hints:   -> wi 3   <-> wb 231   /\ wa 433   /\ w3a 1130   = wceq 1615   e. wcel 1617  A.wral 2385  E.wrex 2386   \ cdif 2856   i^i cin 2858   C_ wss 2859  (/)c0 3114  U.cuni 3398  ` cfv 4163  Topctop 9836  Clsdccld 9947  intcnt 9948  clsccl 9949  Nrmcnrm 16619

This theorem is referenced by:  nrmsep2 16640

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-ral 2389  df-rex 2390  df-rab 2392  df-v 2571  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-nul 3115  df-pw 3261  df-sn 3274  df-pr 3275  df-op 3278  df-uni 3399  df-int 3433  df-br 3540  df-opab 3598  df-id 3779  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-fv 4179  df-top 9842  df-cld 9950  df-ntr 9951  df-cls 9952  df-nrm 16622

Copyright terms: Public domain