Metamath Proof Explorer


Theorem fiint

Description: Equivalent ways of stating the finite intersection property. We show two ways of saying, "the intersection of elements in every finite nonempty subcollection of A is in A ". This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use the left-hand version of this axiom and others the right-hand version, but as our proof here shows, their "intuitively obvious" equivalence can be non-trivial to establish formally. (Contributed by NM, 22-Sep-2002)

Ref Expression
Assertion fiint x A y A x y A x x A x x Fin x A

Proof

Step Hyp Ref Expression
1 isfi x Fin y ω x y
2 ensym x y y x
3 breq1 y = y x x
4 3 anbi2d y = x A x y x x A x x
5 4 imbi1d y = x A x y x x A x A x x x A
6 5 albidv y = x x A x y x x A x x A x x x A
7 breq1 y = v y x v x
8 7 anbi2d y = v x A x y x x A x v x
9 8 imbi1d y = v x A x y x x A x A x v x x A
10 9 albidv y = v x x A x y x x A x x A x v x x A
11 breq1 y = suc v y x suc v x
12 11 anbi2d y = suc v x A x y x x A x suc v x
13 12 imbi1d y = suc v x A x y x x A x A x suc v x x A
14 13 albidv y = suc v x x A x y x x A x x A x suc v x x A
15 ensym x x
16 en0 x x =
17 15 16 sylib x x =
18 17 anim1i x x x = x
19 18 ancoms x x x = x
20 19 adantll x A x x x = x
21 df-ne x ¬ x =
22 pm3.24 ¬ x = ¬ x =
23 22 pm2.21i x = ¬ x = x A
24 21 23 sylan2b x = x x A
25 20 24 syl x A x x x A
26 25 ax-gen x x A x x x A
27 26 a1i z A w A z w A x x A x x x A
28 nfv x z A w A z w A
29 nfa1 x x x A x v x x A
30 bren suc v x f f : suc v 1-1 onto x
31 ssel x A f v x f v A
32 f1of f : suc v 1-1 onto x f : suc v x
33 vex v V
34 33 sucid v suc v
35 ffvelrn f : suc v x v suc v f v x
36 32 34 35 sylancl f : suc v 1-1 onto x f v x
37 31 36 impel x A f : suc v 1-1 onto x f v A
38 37 adantr x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A f v A
39 df-ne f v ¬ f v =
40 imassrn f v ran f
41 dff1o2 f : suc v 1-1 onto x f Fn suc v Fun f -1 ran f = x
42 41 simp3bi f : suc v 1-1 onto x ran f = x
43 40 42 sseqtrid f : suc v 1-1 onto x f v x
44 sstr2 f v x x A f v A
45 43 44 syl f : suc v 1-1 onto x x A f v A
46 45 anim1d f : suc v 1-1 onto x x A f v f v A f v
47 f1of1 f : suc v 1-1 onto x f : suc v 1-1 x
48 vex x V
49 sssucid v suc v
50 f1imaen2g f : suc v 1-1 x x V v suc v v V f v v
51 49 33 50 mpanr12 f : suc v 1-1 x x V f v v
52 47 48 51 sylancl f : suc v 1-1 onto x f v v
53 52 ensymd f : suc v 1-1 onto x v f v
54 46 53 jctird f : suc v 1-1 onto x x A f v f v A f v v f v
55 vex f V
56 55 imaex f v V
57 sseq1 x = f v x A f v A
58 neeq1 x = f v x f v
59 57 58 anbi12d x = f v x A x f v A f v
60 breq2 x = f v v x v f v
61 59 60 anbi12d x = f v x A x v x f v A f v v f v
62 inteq x = f v x = f v
63 62 eleq1d x = f v x A f v A
64 61 63 imbi12d x = f v x A x v x x A f v A f v v f v f v A
65 56 64 spcv x x A x v x x A f v A f v v f v f v A
66 54 65 sylan9 f : suc v 1-1 onto x x x A x v x x A x A f v f v A
67 ineq1 z = f v z w = f v w
68 67 eleq1d z = f v z w A f v w A
69 ineq2 w = f v f v w = f v f v
70 69 eleq1d w = f v f v w A f v f v A
71 68 70 rspc2v f v A f v A z A w A z w A f v f v A
72 71 ex f v A f v A z A w A z w A f v f v A
73 66 72 syl6 f : suc v 1-1 onto x x x A x v x x A x A f v f v A z A w A z w A f v f v A
74 73 com4r z A w A z w A f : suc v 1-1 onto x x x A x v x x A x A f v f v A f v f v A
75 74 exp5c z A w A z w A f : suc v 1-1 onto x x x A x v x x A x A f v f v A f v f v A
76 75 com14 x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A f v f v A f v f v A
77 76 imp43 x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A f v f v A f v f v A
78 39 77 syl5bir x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A ¬ f v = f v A f v f v A
79 inteq f v = f v =
80 int0 = V
81 79 80 eqtrdi f v = f v = V
82 81 ineq1d f v = f v f v = V f v
83 ssv f v V
84 sseqin2 f v V V f v = f v
85 83 84 mpbi V f v = f v
86 82 85 eqtrdi f v = f v f v = f v
87 86 eleq1d f v = f v f v A f v A
88 87 biimprd f v = f v A f v f v A
89 78 88 pm2.61d2 x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A f v A f v f v A
90 38 89 mpd x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A f v f v A
91 fvex f v V
92 91 intunsn f v f v = f v f v
93 f1ofn f : suc v 1-1 onto x f Fn suc v
94 fnsnfv f Fn suc v v suc v f v = f v
95 93 34 94 sylancl f : suc v 1-1 onto x f v = f v
96 95 uneq2d f : suc v 1-1 onto x f v f v = f v f v
97 df-suc suc v = v v
98 97 imaeq2i f suc v = f v v
99 imaundi f v v = f v f v
100 98 99 eqtr2i f v f v = f suc v
101 96 100 eqtrdi f : suc v 1-1 onto x f v f v = f suc v
102 f1ofo f : suc v 1-1 onto x f : suc v onto x
103 foima f : suc v onto x f suc v = x
104 102 103 syl f : suc v 1-1 onto x f suc v = x
105 101 104 eqtrd f : suc v 1-1 onto x f v f v = x
106 105 inteqd f : suc v 1-1 onto x f v f v = x
107 92 106 eqtr3id f : suc v 1-1 onto x f v f v = x
108 107 eleq1d f : suc v 1-1 onto x f v f v A x A
109 108 ad2antlr x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A f v f v A x A
110 90 109 mpbid x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A x A
111 110 exp43 x A f : suc v 1-1 onto x x x A x v x x A z A w A z w A x A
112 111 exlimdv x A f f : suc v 1-1 onto x x x A x v x x A z A w A z w A x A
113 30 112 syl5bi x A suc v x x x A x v x x A z A w A z w A x A
114 113 imp x A suc v x x x A x v x x A z A w A z w A x A
115 114 adantlr x A x suc v x x x A x v x x A z A w A z w A x A
116 115 com13 z A w A z w A x x A x v x x A x A x suc v x x A
117 28 29 116 alrimd z A w A z w A x x A x v x x A x x A x suc v x x A
118 117 a1i v ω z A w A z w A x x A x v x x A x x A x suc v x x A
119 6 10 14 27 118 finds2 y ω z A w A z w A x x A x y x x A
120 sp x x A x y x x A x A x y x x A
121 119 120 syl6 y ω z A w A z w A x A x y x x A
122 121 exp4a y ω z A w A z w A x A x y x x A
123 122 com24 y ω y x x A x z A w A z w A x A
124 2 123 syl5 y ω x y x A x z A w A z w A x A
125 124 rexlimiv y ω x y x A x z A w A z w A x A
126 1 125 sylbi x Fin x A x z A w A z w A x A
127 126 com13 z A w A z w A x A x x Fin x A
128 127 impd z A w A z w A x A x x Fin x A
129 128 alrimiv z A w A z w A x x A x x Fin x A
130 zfpair2 z w V
131 sseq1 x = z w x A z w A
132 neeq1 x = z w x z w
133 131 132 anbi12d x = z w x A x z w A z w
134 eleq1 x = z w x Fin z w Fin
135 133 134 anbi12d x = z w x A x x Fin z w A z w z w Fin
136 inteq x = z w x = z w
137 136 eleq1d x = z w x A z w A
138 135 137 imbi12d x = z w x A x x Fin x A z w A z w z w Fin z w A
139 130 138 spcv x x A x x Fin x A z w A z w z w Fin z w A
140 vex z V
141 vex w V
142 140 141 prss z A w A z w A
143 140 prnz z w
144 143 biantru z w A z w A z w
145 prfi z w Fin
146 145 biantru z w A z w z w A z w z w Fin
147 142 144 146 3bitrri z w A z w z w Fin z A w A
148 140 141 intpr z w = z w
149 148 eleq1i z w A z w A
150 139 147 149 3imtr3g x x A x x Fin x A z A w A z w A
151 150 ralrimivv x x A x x Fin x A z A w A z w A
152 129 151 impbii z A w A z w A x x A x x Fin x A
153 ineq1 x = z x y = z y
154 153 eleq1d x = z x y A z y A
155 ineq2 y = w z y = z w
156 155 eleq1d y = w z y A z w A
157 154 156 cbvral2vw x A y A x y A z A w A z w A
158 df-3an x A x x Fin x A x x Fin
159 158 imbi1i x A x x Fin x A x A x x Fin x A
160 159 albii x x A x x Fin x A x x A x x Fin x A
161 152 157 160 3bitr4i x A y A x y A x x A x x Fin x A