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) Use a separate setvar for the right-hand side and avoid ax-pow . (Revised by BTernaryTau, 14-Jan-2025)

Ref Expression
Assertion fiint 
|- ( A. x e. A A. y e. A ( x i^i y ) e. A <-> A. z ( ( z C_ A /\ z =/= (/) /\ z e. Fin ) -> |^| z e. A ) )

Proof

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