Theorem isnrm2 15552

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 15551	. . 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 749	. 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 924	. . . . . . . . . . . 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		simprr2 925	. . . . . . . . . . . . . . . 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)
5		simplll 452	. . . . . . . . . . . . . . . . 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)
6		difss 2735	. . . . . . . . . . . . . . . . . 18 |- (U.J \ o) C_ U.J
7	6	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)
8		simprlr 457	. . . . . . . . . . . . . . . . 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)
9		incom 2787	. . . . . . . . . . . . . . . . . . . . . 22 |- (o i^i p) = (p i^i o)
10	9	eqeq1i 1891	. . . . . . . . . . . . . . . . . . . . 21 |- ((o i^i p) = (/) <-> (p i^i o) = (/))
11	10	biimpi 168	. . . . . . . . . . . . . . . . . . . 20 |- ((o i^i p) = (/) -> (p i^i o) = (/))
12	11	3ad2ant3 899	. . . . . . . . . . . . . . . . . . 19 |- ((c C_ o /\ d C_ p /\ (o i^i p) = (/)) -> (p i^i o) = (/))
13	12	ad2antll 443	. . . . . . . . . . . . . . . . . 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) = (/))
14		eqid 1884	. . . . . . . . . . . . . . . . . . . . . 22 |- U.J = U.J
15	14	eltopss 8872	. . . . . . . . . . . . . . . . . . . . 21 |- ((J e. Top /\ p e. J) -> p C_ U.J)
16	15	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . . 20 |- (((J e. Top /\ c e. (Clsd` J)) /\ (o e. J /\ p e. J)) -> p C_ U.J)
17	16	ad2ant2r 445	. . . . . . . . . . . . . . . . . . 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)
18		reldisj 2916	. . . . . . . . . . . . . . . . . . 19 |- (p C_ U.J -> ((p i^i o) = (/) <-> p C_ (U.J \ o)))
19	17, 18	syl 12	. . . . . . . . . . . . . . . . . 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)))
20	13, 19	mpbid 212	. . . . . . . . . . . . . . . . 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))
21	14	ssntr 15405	. . . . . . . . . . . . . . . . 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)))
22	5, 7, 8, 20, 21	syl22anc 1101	. . . . . . . . . . . . . . . 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)))
23	4, 22	sstrd 2627	. . . . . . . . . . . . . . 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)))
24	14	eltopss 8872	. . . . . . . . . . . . . . . . . 18 |- ((J e. Top /\ o e. J) -> o C_ U.J)
25	24	ad2ant2r 445	. . . . . . . . . . . . . . . . 17 |- (((J e. Top /\ c e. (Clsd` J)) /\ (o e. J /\ p e. J)) -> o C_ U.J)
26	25	ad2ant2r 445	. . . . . . . . . . . . . . . 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)
27	14	ntrcmp 15406	. . . . . . . . . . . . . . . 16 |- ((J e. Top /\ o C_ U.J) -> ((int` J)` (U.J \ o)) = (U.J \ ((cls` J)` o)))
28	5, 26, 27	syl11anc 524	. . . . . . . . . . . . . . 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)))
29	23, 28	sseqtrd 2653	. . . . . . . . . . . . . 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)))
30	14	cldss 8947	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ d e. (Clsd` J)) -> d C_ U.J)
31	30	ad2ant2r 445	. . . . . . . . . . . . . . . 16 |- (((J e. Top /\ c e. (Clsd` J)) /\ (d e. (Clsd` J) /\ (c i^i d) = (/))) -> d C_ U.J)
32	31	adantr 425	. . . . . . . . . . . . . . 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)
33		reldisj 2916	. . . . . . . . . . . . . . 15 |- (d C_ U.J -> ((d i^i ((cls` J)` o)) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
34	32, 33	syl 12	. . . . . . . . . . . . . 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))))
35	29, 34	mpbird 213	. . . . . . . . . . . . 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)) = (/))
36		incom 2787	. . . . . . . . . . . . 13 |- (((cls` J)` o) i^i d) = (d i^i ((cls` J)` o))
37	35, 36	syl5eq 1940	. . . . . . . . . . . 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 310	. . . . . . . . . . 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 418	. . . . . . . . . 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 418	. . . . . . . . 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 2215	. . . . . . . 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 452	. . . . . . . . . . 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	24	adantlr 429	. . . . . . . . . . . 12 |- (((J e. Top /\ c e. (Clsd` J)) /\ o e. J) -> o C_ U.J)
44	43	ad2ant2r 445	. . . . . . . . . . 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	14	cmclsopn 8969	. . . . . . . . . . 11 |- ((J e. Top /\ o C_ U.J) -> (U.J \ ((cls` J)` o)) e. J)
46	42, 44, 45	syl11anc 524	. . . . . . . . . 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 458	. . . . . . . . . 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	30, 33	syl 12	. . . . . . . . . . . . . . . . 17 |- ((J e. Top /\ d e. (Clsd` J)) -> ((d i^i ((cls` J)` o)) = (/) <-> d C_ (U.J \ ((cls` J)` o))))
49	48	ad2ant2r 445	. . . . . . . . . . . . . . . 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))))
50	49	adantr 425	. . . . . . . . . . . . . . 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))))
51	36	eqeq1i 1891	. . . . . . . . . . . . . . 15 |- ((((cls` J)` o) i^i d) = (/) <-> (d i^i ((cls` J)` o)) = (/))
52	50, 51	syl5bb 591	. . . . . . . . . . . . . 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 170	. . . . . . . . . . . . 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 418	. . . . . . . . . . . 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 388	. . . . . . . . . . 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 422	. . . . . . . . . 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	14	sscls 8965	. . . . . . . . . . . . . 14 |- ((J e. Top /\ o C_ U.J) -> o C_ ((cls` J)` o))
58	42, 44, 57	syl11anc 524	. . . . . . . . . . . . 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 2817	. . . . . . . . . . . . 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 12	. . . . . . . . . . . 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 2945	. . . . . . . . . . . 12 |- (((cls` J)` o) i^i (U.J \ ((cls` J)` o))) = (/)
62	60, 61	syl6ss 2663	. . . . . . . . . . 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 2902	. . . . . . . . . . 11 |- ((o i^i (U.J \ ((cls` J)` o))) C_ (/) -> (o i^i (U.J \ ((cls` J)` o))) = (/))
64	62, 63	syl 12	. . . . . . . . . 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 2639	. . . . . . . . . . . 12 |- (p = (U.J \ ((cls` J)` o)) -> (d C_ p <-> d C_ (U.J \ ((cls` J)` o))))
66		ineq2 2790	. . . . . . . . . . . . 13 |- (p = (U.J \ ((cls` J)` o)) -> (o i^i p) = (o i^i (U.J \ ((cls` J)` o))))
67	66	eqeq1d 1892	. . . . . . . . . . . 12 |- (p = (U.J \ ((cls` J)` o)) -> ((o i^i p) = (/) <-> (o i^i (U.J \ ((cls` J)` o))) = (/)))
68	65, 67	3anbi23d 1171	. . . . . . . . . . 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 2381	. . . . . . . . . 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 1102	. . . . . . . . 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 418	. . . . . . . 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 574	. . . . . . 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 2120	. . . . . 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 418	. . . . 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 645	. . . 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 2119	. . 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 2119	. 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 587	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 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106   \ cdif 2590   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177  ` cfv 3998  Topctop 8857  Clsdccld 8936  intcnt 8937  clsccl 8938  Nrmcnrm 15534

This theorem is referenced by:  nrmsep2 15555

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

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  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-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-int 3215  df-br 3339  df-opab 3396  df-id 3586  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-fv 4014  df-top 8861  df-cld 8939  df-ntr 8940  df-cls 8941  df-nrm 15537

Copyright terms: Public domain