Table of ContentsTable of Contents Mathbox for Frédéric Liné < Previous   Next >
Related theorems
Unicode version
Theorem cnfilca 14927
Description: Condition to have a filter finer than a given filter and containing a set A. Bourbaki T.G. I.37 cor. 1
Assertion
Ref Expression
cnfilca |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F C_ g) <-> A.x e. F (x i^i A) =/= (/)))
Distinct variable groups:   A,g   x,A   g,F   x,F
Proof of Theorem cnfilca
StepHypRef Expression
1 ssexg 3457 . . . . . . 7 |- ((A C_ U.F /\ U.F e. _V) -> A e. _V)
2 uniexg 3795 . . . . . . 7 |- (F e. Fil -> U.F e. _V)
31, 2sylan2 500 . . . . . 6 |- ((A C_ U.F /\ F e. Fil) -> A e. _V)
43ancoms 484 . . . . 5 |- ((F e. Fil /\ A C_ U.F) -> A e. _V)
543adant3 896 . . . 4 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> A e. _V)
6 snssg 3124 . . . . . 6 |- (A e. _V -> (A e. g <-> {A} C_ g))
76anbi1d 679 . . . . 5 |- (A e. _V -> ((A e. g /\ F C_ g) <-> ({A} C_ g /\ F C_ g)))
8 unss 2780 . . . . 5 |- (({A} C_ g /\ F C_ g) <-> ({A} u. F) C_ g)
97, 8syl6bb 595 . . . 4 |- (A e. _V -> ((A e. g /\ F C_ g) <-> ({A} u. F) C_ g))
105, 9syl 12 . . 3 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> ((A e. g /\ F C_ g) <-> ({A} u. F) C_ g))
1110rexbidv 2124 . 2 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F C_ g) <-> E.g e. Fil ({A} u. F) C_ g))
121ex 402 . . . . . . 7 |- (A C_ U.F -> (U.F e. _V -> A e. _V))
13 elpwg 3038 . . . . . . . . 9 |- (A e. _V -> (A e. ~PU.F <-> A C_ U.F))
14 snssg 3124 . . . . . . . . 9 |- (A e. _V -> (A e. ~PU.F <-> {A} C_ ~PU.F))
1513, 14bitr3d 589 . . . . . . . 8 |- (A e. _V -> (A C_ U.F <-> {A} C_ ~PU.F))
16 pwuni 3505 . . . . . . . . 9 |- F C_ ~PU.F
17 unss 2780 . . . . . . . . . 10 |- (({A} C_ ~PU.F /\ F C_ ~PU.F) <-> ({A} u. F) C_ ~PU.F)
1817biimpi 168 . . . . . . . . 9 |- (({A} C_ ~PU.F /\ F C_ ~PU.F) -> ({A} u. F) C_ ~PU.F)
1916, 18mpan2 760 . . . . . . . 8 |- ({A} C_ ~PU.F -> ({A} u. F) C_ ~PU.F)
2015, 19syl6bi 231 . . . . . . 7 |- (A e. _V -> (A C_ U.F -> ({A} u. F) C_ ~PU.F))
2112, 20syl6 25 . . . . . 6 |- (A C_ U.F -> (U.F e. _V -> (A C_ U.F -> ({A} u. F) C_ ~PU.F)))
2221pm2.43a 80 . . . . 5 |- (A C_ U.F -> (U.F e. _V -> ({A} u. F) C_ ~PU.F))
232, 22mpan9 521 . . . 4 |- ((F e. Fil /\ A C_ U.F) -> ({A} u. F) C_ ~PU.F)
24233adant3 896 . . 3 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> ({A} u. F) C_ ~PU.F)
2523ad2ant1 897 . . 3 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> U.F e. _V)
26 emnfil 10273 . . . . 5 |- -. (/) e. Fil
27 nelneq 1985 . . . . . 6 |- ((F e. Fil /\ -. (/) e. Fil) -> -. F = (/))
28 simpr 350 . . . . . . . 8 |- (({A} = (/) /\ F = (/)) -> F = (/))
2928con3i 114 . . . . . . 7 |- (-. F = (/) -> -. ({A} = (/) /\ F = (/)))
30 un00 2907 . . . . . . . 8 |- (({A} = (/) /\ F = (/)) <-> ({A} u. F) = (/))
3130necon3bbii 2031 . . . . . . 7 |- (-. ({A} = (/) /\ F = (/)) <-> ({A} u. F) =/= (/))
3229, 31sylib 215 . . . . . 6 |- (-. F = (/) -> ({A} u. F) =/= (/))
3327, 32syl 12 . . . . 5 |- ((F e. Fil /\ -. (/) e. Fil) -> ({A} u. F) =/= (/))
3426, 33mpan2 760 . . . 4 |- (F e. Fil -> ({A} u. F) =/= (/))
35343ad2ant1 897 . . 3 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> ({A} u. F) =/= (/))
36 efilcp2 14926 . . 3 |- ((({A} u. F) C_ ~PU.F /\ U.F e. _V /\ ({A} u. F) =/= (/)) -> (-. (/) e. ( fi ` ({A} u. F)) <-> E.g e. Fil ({A} u. F) C_ g))
3724, 25, 35, 36syl111anc 1100 . 2 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (-. (/) e. ( fi ` ({A} u. F)) <-> E.g e. Fil ({A} u. F) C_ g))
38 elisset 2299 . . . . . . . 8 |- (F e. Fil -> F e. _V)
39383ad2ant1 897 . . . . . . 7 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> F e. _V)
40 snex 3492 . . . . . . 7 |- {A} e. _V
4139, 40jctil 316 . . . . . 6 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> ({A} e. _V /\ F e. _V))
42 unexb 3797 . . . . . 6 |- (({A} e. _V /\ F e. _V) <-> ({A} u. F) e. _V)
4341, 42sylib 215 . . . . 5 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> ({A} u. F) e. _V)
44 0ex 3446 . . . . 5 |- (/) e. _V
4543, 44jctil 316 . . . 4 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> ((/) e. _V /\ ({A} u. F) e. _V))
46 sppfi 10218 . . . . 5 |- (((/) e. _V /\ ({A} u. F) e. _V) -> ((/) e. ( fi ` ({A} u. F)) <-> E.y(y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y)))
4746notbid 673 . . . 4 |- (((/) e. _V /\ ({A} u. F) e. _V) -> (-. (/) e. ( fi ` ({A} u. F)) <-> -. E.y(y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y)))
4845, 47syl 12 . . 3 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (-. (/) e. ( fi ` ({A} u. F)) <-> -. E.y(y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y)))
49 ax-17 1317 . . . . . 6 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) -> A.x((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)))
50 elun2 2772 . . . . . . . . . . . . . . . . . 18 |- (x e. F -> x e. ({A} u. F))
5150adantl 424 . . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> x e. ({A} u. F))
52 snidg 3067 . . . . . . . . . . . . . . . . . . . 20 |- (A e. _V -> A e. {A})
53 elun1 2771 . . . . . . . . . . . . . . . . . . . 20 |- (A e. {A} -> A e. ({A} u. F))
5452, 53syl 12 . . . . . . . . . . . . . . . . . . 19 |- (A e. _V -> A e. ({A} u. F))
555, 54syl 12 . . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> A e. ({A} u. F))
5655adantr 425 . . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> A e. ({A} u. F))
5751, 56jca 310 . . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> (x e. ({A} u. F) /\ A e. ({A} u. F)))
58 simpr 350 . . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> x e. F)
59 simp2 877 . . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> A C_ U.F)
605, 13syl 12 . . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (A e. ~PU.F <-> A C_ U.F))
6159, 60mpbird 213 . . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> A e. ~PU.F)
6261adantr 425 . . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> A e. ~PU.F)
63 prssg 3140 . . . . . . . . . . . . . . . . . 18 |- ((x e. F /\ A e. ~PU.F) -> ((x e. ({A} u. F) /\ A e. ({A} u. F)) <-> {x, A} C_ ({A} u. F)))
6463bicomd 580 . . . . . . . . . . . . . . . . 17 |- ((x e. F /\ A e. ~PU.F) -> ({x, A} C_ ({A} u. F) <-> (x e. ({A} u. F) /\ A e. ({A} u. F))))
6558, 62, 64syl11anc 524 . . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> ({x, A} C_ ({A} u. F) <-> (x e. ({A} u. F) /\ A e. ({A} u. F))))
6657, 65mpbird 213 . . . . . . . . . . . . . . 15 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> {x, A} C_ ({A} u. F))
67 prfi 5647 . . . . . . . . . . . . . . 15 |- {x, A} e. Fin
6866, 67jctir 317 . . . . . . . . . . . . . 14 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> ({x, A} C_ ({A} u. F) /\ {x, A} e. Fin))
69 prex 3526 . . . . . . . . . . . . . . . 16 |- {x, A} e. _V
7069a1i 8 . . . . . . . . . . . . . . 15 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> {x, A} e. _V)
71 sseq1 2637 . . . . . . . . . . . . . . . . . 18 |- (y = {x, A} -> (y C_ ({A} u. F) <-> {x, A} C_ ({A} u. F)))
72 eleq1 1957 . . . . . . . . . . . . . . . . . 18 |- (y = {x, A} -> (y e. Fin <-> {x, A} e. Fin))
7371, 72anbi12d 690 . . . . . . . . . . . . . . . . 17 |- (y = {x, A} -> ((y C_ ({A} u. F) /\ y e. Fin) <-> ({x, A} C_ ({A} u. F) /\ {x, A} e. Fin)))
74 inteq 3217 . . . . . . . . . . . . . . . . . . 19 |- (y = {x, A} -> |^|y = |^|{x, A})
7574eqeq2d 1895 . . . . . . . . . . . . . . . . . 18 |- (y = {x, A} -> ((/) = |^|y <-> (/) = |^|{x, A}))
7675notbid 673 . . . . . . . . . . . . . . . . 17 |- (y = {x, A} -> (-. (/) = |^|y <-> -. (/) = |^|{x, A}))
7773, 76imbi12d 688 . . . . . . . . . . . . . . . 16 |- (y = {x, A} -> (((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) <-> (({x, A} C_ ({A} u. F) /\ {x, A} e. Fin) -> -. (/) = |^|{x, A})))
7877cla4gv 2364 . . . . . . . . . . . . . . 15 |- ({x, A} e. _V -> (A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) -> (({x, A} C_ ({A} u. F) /\ {x, A} e. Fin) -> -. (/) = |^|{x, A})))
7970, 78syl 12 . . . . . . . . . . . . . 14 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> (A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) -> (({x, A} C_ ({A} u. F) /\ {x, A} e. Fin) -> -. (/) = |^|{x, A})))
8068, 79mpid 58 . . . . . . . . . . . . 13 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ x e. F) -> (A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) -> -. (/) = |^|{x, A}))
8180ex 402 . . . . . . . . . . . 12 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (x e. F -> (A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) -> -. (/) = |^|{x, A})))
8281com23 36 . . . . . . . . . . 11 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) -> (x e. F -> -. (/) = |^|{x, A})))
8382imp31 389 . . . . . . . . . 10 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> -. (/) = |^|{x, A})
84 df-ne 2019 . . . . . . . . . 10 |- ((/) =/= |^|{x, A} <-> -. (/) = |^|{x, A})
8583, 84sylibr 217 . . . . . . . . 9 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> (/) =/= |^|{x, A})
8685necomd 2095 . . . . . . . 8 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> |^|{x, A} =/= (/))
875ad2antrr 440 . . . . . . . . . . . 12 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> A e. _V)
88 visset 2295 . . . . . . . . . . . 12 |- x e. _V
8987, 88jctil 316 . . . . . . . . . . 11 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> (x e. _V /\ A e. _V))
90 intprg 3251 . . . . . . . . . . 11 |- ((x e. _V /\ A e. _V) -> |^|{x, A} = (x i^i A))
9189, 90syl 12 . . . . . . . . . 10 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> |^|{x, A} = (x i^i A))
9291eqcomd 1889 . . . . . . . . 9 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> (x i^i A) = |^|{x, A})
9392neeq1d 2028 . . . . . . . 8 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> ((x i^i A) =/= (/) <-> |^|{x, A} =/= (/)))
9486, 93mpbird 213 . . . . . . 7 |- ((((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) /\ x e. F) -> (x i^i A) =/= (/))
9594ex 402 . . . . . 6 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) -> (x e. F -> (x i^i A) =/= (/)))
9649, 95r19.21ai 2174 . . . . 5 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) -> A.x e. F (x i^i A) =/= (/))
97 moec 14351 . . . . . . . 8 |- (A e. y -> |^|y = (A i^i |^|(y \ {A})))
98 ssundif 2955 . . . . . . . . . . 11 |- (y C_ ({A} u. F) <-> (y \ {A}) C_ F)
99 inteq 3217 . . . . . . . . . . . . . . . . . . . . 21 |- ((y \ {A}) = (/) -> |^|(y \ {A}) = |^|(/))
100 int0 3230 . . . . . . . . . . . . . . . . . . . . . 22 |- |^|(/) = _V
101 eqtr 1904 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((|^|(y \ {A}) = |^|(/) /\ |^|(/) = _V) -> |^|(y \ {A}) = _V)
102101ex 402 . . . . . . . . . . . . . . . . . . . . . . 23 |- (|^|(y \ {A}) = |^|(/) -> (|^|(/) = _V -> |^|(y \ {A}) = _V))
103 ineq2 2790 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (|^|(y \ {A}) = _V -> (A i^i |^|(y \ {A})) = (A i^i _V))
104 inv1 2898 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (A i^i _V) = A
105 eqtr 1904 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((A i^i |^|(y \ {A})) = (A i^i _V) /\ (A i^i _V) = A) -> (A i^i |^|(y \ {A})) = A)
106105ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A i^i |^|(y \ {A})) = (A i^i _V) -> ((A i^i _V) = A -> (A i^i |^|(y \ {A})) = A))
107 eqtr 1904 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((|^|y = (A i^i |^|(y \ {A})) /\ (A i^i |^|(y \ {A})) = A) -> |^|y = A)
108107ex 402 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (|^|y = (A i^i |^|(y \ {A})) -> ((A i^i |^|(y \ {A})) = A -> |^|y = A))
109 neeq1 2024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (A = |^|y -> (A =/= (/) <-> |^|y =/= (/)))
110 necom 2094 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (|^|y =/= (/) <-> (/) =/= |^|y)
111 df-ne 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((/) =/= |^|y <-> -. (/) = |^|y)
112111biimpi 168 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((/) =/= |^|y -> -. (/) = |^|y)
113110, 112sylbi 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (|^|y =/= (/) -> -. (/) = |^|y)
114109, 113syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (A = |^|y -> (A =/= (/) -> -. (/) = |^|y))
115114eqcoms 1887 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (|^|y = A -> (A =/= (/) -> -. (/) = |^|y))
116108, 115syl6 25 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (|^|y = (A i^i |^|(y \ {A})) -> ((A i^i |^|(y \ {A})) = A -> (A =/= (/) -> -. (/) = |^|y)))
117116com3l 38 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((A i^i |^|(y \ {A})) = A -> (A =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
118106, 117syl6 25 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((A i^i |^|(y \ {A})) = (A i^i _V) -> ((A i^i _V) = A -> (A =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
119104, 118mpi 55 . . . . . . . . . . . . . . . . . . . . . . . 24 |- ((A i^i |^|(y \ {A})) = (A i^i _V) -> (A =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
120103, 119syl 12 . . . . . . . . . . . . . . . . . . . . . . 23 |- (|^|(y \ {A}) = _V -> (A =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
121102, 120syl6com 64 . . . . . . . . . . . . . . . . . . . . . 22 |- (|^|(/) = _V -> (|^|(y \ {A}) = |^|(/) -> (A =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
122100, 121ax-mp 7 . . . . . . . . . . . . . . . . . . . . 21 |- (|^|(y \ {A}) = |^|(/) -> (A =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
12399, 122syl 12 . . . . . . . . . . . . . . . . . . . 20 |- ((y \ {A}) = (/) -> (A =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
124123com12 14 . . . . . . . . . . . . . . . . . . 19 |- (A =/= (/) -> ((y \ {A}) = (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
125124a1i 8 . . . . . . . . . . . . . . . . . 18 |- ((y \ {A}) C_ F -> (A =/= (/) -> ((y \ {A}) = (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
126125a1i 8 . . . . . . . . . . . . . . . . 17 |- (A.x e. F (x i^i A) =/= (/) -> ((y \ {A}) C_ F -> (A =/= (/) -> ((y \ {A}) = (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))))
127126a1i 8 . . . . . . . . . . . . . . . 16 |- (y e. Fin -> (A.x e. F (x i^i A) =/= (/) -> ((y \ {A}) C_ F -> (A =/= (/) -> ((y \ {A}) = (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
128127com14 42 . . . . . . . . . . . . . . 15 |- (A =/= (/) -> (A.x e. F (x i^i A) =/= (/) -> ((y \ {A}) C_ F -> (y e. Fin -> ((y \ {A}) = (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
1291283ad2ant3 899 . . . . . . . . . . . . . 14 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (A.x e. F (x i^i A) =/= (/) -> ((y \ {A}) C_ F -> (y e. Fin -> ((y \ {A}) = (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
130129imp 377 . . . . . . . . . . . . 13 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> ((y \ {A}) C_ F -> (y e. Fin -> ((y \ {A}) = (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))))
131130com14 42 . . . . . . . . . . . 12 |- ((y \ {A}) = (/) -> ((y \ {A}) C_ F -> (y e. Fin -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))))
132 difss 2735 . . . . . . . . . . . . 13 |- (y \ {A}) C_ y
133 ssfi 5630 . . . . . . . . . . . . . . . 16 |- ((y e. Fin /\ (y \ {A}) C_ y) -> (y \ {A}) e. Fin)
134133ex 402 . . . . . . . . . . . . . . 15 |- (y e. Fin -> ((y \ {A}) C_ y -> (y \ {A}) e. Fin))
135 simp1 876 . . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> F e. Fil)
136 df-ne 2019 . . . . . . . . . . . . . . . . . . . . . 22 |- ((y \ {A}) =/= (/) <-> -. (y \ {A}) = (/))
137 filint2 14923 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F e. Fil -> (((y \ {A}) C_ F /\ (y \ {A}) =/= (/) /\ (y \ {A}) e. Fin) -> |^|(y \ {A}) e. F))
138 ineq1 2789 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = |^|(y \ {A}) -> (x i^i A) = (|^|(y \ {A}) i^i A))
139138neeq1d 2028 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x = |^|(y \ {A}) -> ((x i^i A) =/= (/) <-> (|^|(y \ {A}) i^i A) =/= (/)))
140139rcla4v 2376 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (|^|(y \ {A}) e. F -> (A.x e. F (x i^i A) =/= (/) -> (|^|(y \ {A}) i^i A) =/= (/)))
141 incom 2787 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (|^|(y \ {A}) i^i A) = (A i^i |^|(y \ {A}))
142 neeq1 2024 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((|^|(y \ {A}) i^i A) = (A i^i |^|(y \ {A})) -> ((|^|(y \ {A}) i^i A) =/= (/) <-> (A i^i |^|(y \ {A})) =/= (/)))
143 neeq1 2024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((A i^i |^|(y \ {A})) = |^|y -> ((A i^i |^|(y \ {A})) =/= (/) <-> |^|y =/= (/)))
144143biimpd 170 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((A i^i |^|(y \ {A})) = |^|y -> ((A i^i |^|(y \ {A})) =/= (/) -> |^|y =/= (/)))
145144eqcoms 1887 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (|^|y = (A i^i |^|(y \ {A})) -> ((A i^i |^|(y \ {A})) =/= (/) -> |^|y =/= (/)))
146145, 113syl6com 64 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((A i^i |^|(y \ {A})) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))
147142, 146syl6bi 231 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((|^|(y \ {A}) i^i A) = (A i^i |^|(y \ {A})) -> ((|^|(y \ {A}) i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
148141, 147ax-mp 7 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((|^|(y \ {A}) i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))
149140, 148syl6 25 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (|^|(y \ {A}) e. F -> (A.x e. F (x i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
150137, 149syl6 25 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (F e. Fil -> (((y \ {A}) C_ F /\ (y \ {A}) =/= (/) /\ (y \ {A}) e. Fin) -> (A.x e. F (x i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
1511503expd 1085 . . . . . . . . . . . . . . . . . . . . . . 23 |- (F e. Fil -> ((y \ {A}) C_ F -> ((y \ {A}) =/= (/) -> ((y \ {A}) e. Fin -> (A.x e. F (x i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
152151com13 37 . . . . . . . . . . . . . . . . . . . . . 22 |- ((y \ {A}) =/= (/) -> ((y \ {A}) C_ F -> (F e. Fil -> ((y \ {A}) e. Fin -> (A.x e. F (x i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
153136, 152sylbir 218 . . . . . . . . . . . . . . . . . . . . 21 |- (-. (y \ {A}) = (/) -> ((y \ {A}) C_ F -> (F e. Fil -> ((y \ {A}) e. Fin -> (A.x e. F (x i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
154153com13 37 . . . . . . . . . . . . . . . . . . . 20 |- (F e. Fil -> ((y \ {A}) C_ F -> (-. (y \ {A}) = (/) -> ((y \ {A}) e. Fin -> (A.x e. F (x i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
1551543imp 1061 . . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ (y \ {A}) C_ F /\ -. (y \ {A}) = (/)) -> ((y \ {A}) e. Fin -> (A.x e. F (x i^i A) =/= (/) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
156155com3r 39 . . . . . . . . . . . . . . . . . 18 |- (A.x e. F (x i^i A) =/= (/) -> ((F e. Fil /\ (y \ {A}) C_ F /\ -. (y \ {A}) = (/)) -> ((y \ {A}) e. Fin -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
1571563expd 1085 . . . . . . . . . . . . . . . . 17 |- (A.x e. F (x i^i A) =/= (/) -> (F e. Fil -> ((y \ {A}) C_ F -> (-. (y \ {A}) = (/) -> ((y \ {A}) e. Fin -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
158135, 157mpan9 521 . . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> ((y \ {A}) C_ F -> (-. (y \ {A}) = (/) -> ((y \ {A}) e. Fin -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))))
159158com14 42 . . . . . . . . . . . . . . 15 |- ((y \ {A}) e. Fin -> ((y \ {A}) C_ F -> (-. (y \ {A}) = (/) -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))))
160134, 159syl6 25 . . . . . . . . . . . . . 14 |- (y e. Fin -> ((y \ {A}) C_ y -> ((y \ {A}) C_ F -> (-. (y \ {A}) = (/) -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
161160com14 42 . . . . . . . . . . . . 13 |- (-. (y \ {A}) = (/) -> ((y \ {A}) C_ y -> ((y \ {A}) C_ F -> (y e. Fin -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))))
162132, 161mpi 55 . . . . . . . . . . . 12 |- (-. (y \ {A}) = (/) -> ((y \ {A}) C_ F -> (y e. Fin -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))))
163131, 162pm2.61i 140 . . . . . . . . . . 11 |- ((y \ {A}) C_ F -> (y e. Fin -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
16498, 163sylbi 216 . . . . . . . . . 10 |- (y C_ ({A} u. F) -> (y e. Fin -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y))))
165164imp 377 . . . . . . . . 9 |- ((y C_ ({A} u. F) /\ y e. Fin) -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (|^|y = (A i^i |^|(y \ {A})) -> -. (/) = |^|y)))
166165com13 37 . . . . . . . 8 |- (|^|y = (A i^i |^|(y \ {A})) -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> ((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)))
16797, 166syl 12 . . . . . . 7 |- (A e. y -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> ((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)))
168 elsni 3066 . . . . . . . . . . . . . . . . . 18 |- (x e. {A} -> x = A)
169 eleq1 1957 . . . . . . . . . . . . . . . . . . 19 |- (x = A -> (x e. y <-> A e. y))
170169biimpd 170 . . . . . . . . . . . . . . . . . 18 |- (x = A -> (x e. y -> A e. y))
171168, 170syl 12 . . . . . . . . . . . . . . . . 17 |- (x e. {A} -> (x e. y -> A e. y))
172171com12 14 . . . . . . . . . . . . . . . 16 |- (x e. y -> (x e. {A} -> A e. y))
173172con3d 111 . . . . . . . . . . . . . . 15 |- (x e. y -> (-. A e. y -> -. x e. {A}))
174173com12 14 . . . . . . . . . . . . . 14 |- (-. A e. y -> (x e. y -> -. x e. {A}))
17517419.21aiv 1664 . . . . . . . . . . . . 13 |- (-. A e. y -> A.x(x e. y -> -. x e. {A}))
176 disj1 2915 . . . . . . . . . . . . 13 |- ((y i^i {A}) = (/) <-> A.x(x e. y -> -. x e. {A}))
177175, 176sylibr 217 . . . . . . . . . . . 12 |- (-. A e. y -> (y i^i {A}) = (/))
178 disjssun 2932 . . . . . . . . . . . . 13 |- ((y i^i {A}) = (/) -> (y C_ ({A} u. F) <-> y C_ F))
179178biimpd 170 . . . . . . . . . . . 12 |- ((y i^i {A}) = (/) -> (y C_ ({A} u. F) -> y C_ F))
180177, 179syl 12 . . . . . . . . . . 11 |- (-. A e. y -> (y C_ ({A} u. F) -> y C_ F))
181 inteq 3217 . . . . . . . . . . . . . . . . . . . 20 |- (y = (/) -> |^|y = |^|(/))
182 eqtr 1904 . . . . . . . . . . . . . . . . . . . . . . 23 |- ((|^|y = |^|(/) /\ |^|(/) = _V) -> |^|y = _V)
183182ex 402 . . . . . . . . . . . . . . . . . . . . . 22 |- (|^|y = |^|(/) -> (|^|(/) = _V -> |^|y = _V))
184 vn0 2882 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- _V =/= (/)
185 necom 2094 . . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (_V =/= (/) <-> (/) =/= _V)
186184, 185mpbi 206 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (/) =/= _V
187 neeq2 2025 . . . . . . . . . . . . . . . . . . . . . . . . 25 |- (_V = |^|y -> ((/) =/= _V <-> (/) =/= |^|y))
188186, 187mpbii 210 . . . . . . . . . . . . . . . . . . . . . . . 24 |- (_V = |^|y -> (/) =/= |^|y)
189188, 111sylib 215 . . . . . . . . . . . . . . . . . . . . . . 23 |- (_V = |^|y -> -. (/) = |^|y)
190189eqcoms 1887 . . . . . . . . . . . . . . . . . . . . . 22 |- (|^|y = _V -> -. (/) = |^|y)
191183, 190syl6 25 . . . . . . . . . . . . . . . . . . . . 21 |- (|^|y = |^|(/) -> (|^|(/) = _V -> -. (/) = |^|y))
192100, 191mpi 55 . . . . . . . . . . . . . . . . . . . 20 |- (|^|y = |^|(/) -> -. (/) = |^|y)
193181, 192syl 12 . . . . . . . . . . . . . . . . . . 19 |- (y = (/) -> -. (/) = |^|y)
194193a1i 8 . . . . . . . . . . . . . . . . . 18 |- (y C_ F -> (y = (/) -> -. (/) = |^|y))
195194a1i 8 . . . . . . . . . . . . . . . . 17 |- (F e. Fil -> (y C_ F -> (y = (/) -> -. (/) = |^|y)))
196195a1i 8 . . . . . . . . . . . . . . . 16 |- (y e. Fin -> (F e. Fil -> (y C_ F -> (y = (/) -> -. (/) = |^|y))))
197196com14 42 . . . . . . . . . . . . . . 15 |- (y = (/) -> (F e. Fil -> (y C_ F -> (y e. Fin -> -. (/) = |^|y))))
198 fipfil2 10272 . . . . . . . . . . . . . . . . . . . 20 |- (F e. Fil -> ((y C_ F /\ y =/= (/) /\ y e. Fin) -> |^|y =/= (/)))
199198imp 377 . . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ (y C_ F /\ y =/= (/) /\ y e. Fin)) -> |^|y =/= (/))
200199necomd 2095 . . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ (y C_ F /\ y =/= (/) /\ y e. Fin)) -> (/) =/= |^|y)
201200, 111sylib 215 . . . . . . . . . . . . . . . . 17 |- ((F e. Fil /\ (y C_ F /\ y =/= (/) /\ y e. Fin)) -> -. (/) = |^|y)
2022013exp2 1086 . . . . . . . . . . . . . . . 16 |- (F e. Fil -> (y C_ F -> (y =/= (/) -> (y e. Fin -> -. (/) = |^|y))))
203202com3r 39 . . . . . . . . . . . . . . 15 |- (y =/= (/) -> (F e. Fil -> (y C_ F -> (y e. Fin -> -. (/) = |^|y))))
204197, 203pm2.61ine 2089 . . . . . . . . . . . . . 14 |- (F e. Fil -> (y C_ F -> (y e. Fin -> -. (/) = |^|y)))
2052043ad2ant1 897 . . . . . . . . . . . . 13 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (y C_ F -> (y e. Fin -> -. (/) = |^|y)))
206205adantr 425 . . . . . . . . . . . 12 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (y C_ F -> (y e. Fin -> -. (/) = |^|y)))
207206com12 14 . . . . . . . . . . 11 |- (y C_ F -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (y e. Fin -> -. (/) = |^|y)))
208180, 207syl6com 64 . . . . . . . . . 10 |- (y C_ ({A} u. F) -> (-. A e. y -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (y e. Fin -> -. (/) = |^|y))))
209208com24 41 . . . . . . . . 9 |- (y C_ ({A} u. F) -> (y e. Fin -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (-. A e. y -> -. (/) = |^|y))))
210209imp 377 . . . . . . . 8 |- ((y C_ ({A} u. F) /\ y e. Fin) -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> (-. A e. y -> -. (/) = |^|y)))
211210com13 37 . . . . . . 7 |- (-. A e. y -> (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> ((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)))
212167, 211pm2.61i 140 . . . . . 6 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> ((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y))
21321219.21aiv 1664 . . . . 5 |- (((F e. Fil /\ A C_ U.F /\ A =/= (/)) /\ A.x e. F (x i^i A) =/= (/)) -> A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y))
21496, 213impbida 577 . . . 4 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) <-> A.x e. F (x i^i A) =/= (/)))
215 alnex 1380 . . . . 5 |- (A.y -. (y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y) <-> -. E.y(y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y))
216 df-3an 860 . . . . . . . 8 |- ((y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y) <-> ((y C_ ({A} u. F) /\ y e. Fin) /\ (/) = |^|y))
217216notbii 204 . . . . . . 7 |- (-. (y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y) <-> -. ((y C_ ({A} u. F) /\ y e. Fin) /\ (/) = |^|y))
218 imnan 261 . . . . . . 7 |- (((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y) <-> -. ((y C_ ({A} u. F) /\ y e. Fin) /\ (/) = |^|y))
219217, 218bitr4i 193 . . . . . 6 |- (-. (y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y) <-> ((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y))
220219albii 1346 . . . . 5 |- (A.y -. (y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y) <-> A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y))
221215, 220bitr3i 192 . . . 4 |- (-. E.y(y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y) <-> A.y((y C_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y))
222214, 221syl5bb 591 . . 3 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (-. E.y(y C_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y) <-> A.x e. F (x i^i A) =/= (/)))
22348, 222bitrd 587 . 2 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (-. (/) e. ( fi ` ({A} u. F)) <-> A.x e. F (x i^i A) =/= (/)))
22411, 37, 2233bitr2d 605 1 |- ((F e. Fil /\ A C_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F C_ g) <-> A.x e. F (x i^i A) =/= (/)))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326   =/= wne 2017  A.wral 2105  E.wrex 2106  _Vcvv 2292   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  {cpr 3045  U.cuni 3177  |^|cint 3214  ` cfv 3998  Fincfn 5426   fi cfi 10210  Filcfil 10264
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-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-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-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211  df-fil 10265
Copyright terms: Public domain