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 
|- ( A. x e. A A. y e. A ( x i^i y ) e. A <-> A. x ( ( x C_ A /\ x =/= (/) /\ x e. Fin ) -> |^| x e. A ) )

Proof

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