Metamath Proof Explorer

Theorem disjinfi

Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set C . (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses disjinfi.b 
|- ( ( ph /\ x e. A ) -> B e. V )
disjinfi.d 
|- ( ph -> Disj_ x e. A B )
disjinfi.c 
|- ( ph -> C e. Fin )
Assertion disjinfi 
|- ( ph -> { x e. A | ( B i^i C ) =/= (/) } e. Fin )

Proof

Step Hyp Ref Expression
1 disjinfi.b 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 disjinfi.d 
 |-  ( ph -> Disj_ x e. A B )
3 disjinfi.c 
 |-  ( ph -> C e. Fin )
4 inss2 
 |-  ( U. ran ( x e. A |-> B ) i^i C ) C_ C
5 ssfi 
 |-  ( ( C e. Fin /\ ( U. ran ( x e. A |-> B ) i^i C ) C_ C ) -> ( U. ran ( x e. A |-> B ) i^i C ) e. Fin )
6 3 4 5 sylancl 
 |-  ( ph -> ( U. ran ( x e. A |-> B ) i^i C ) e. Fin )
7 4 a1i 
 |-  ( ph -> ( U. ran ( x e. A |-> B ) i^i C ) C_ C )
8 3 7 ssexd 
 |-  ( ph -> ( U. ran ( x e. A |-> B ) i^i C ) e. _V )
9 elinel1 
 |-  ( y e. ( U. ran ( x e. A |-> B ) i^i C ) -> y e. U. ran ( x e. A |-> B ) )
10 eluni2 
 |-  ( y e. U. ran ( x e. A |-> B ) <-> E. w e. ran ( x e. A |-> B ) y e. w )
11 10 biimpi 
 |-  ( y e. U. ran ( x e. A |-> B ) -> E. w e. ran ( x e. A |-> B ) y e. w )
12 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
13 12 elrnmpt 
 |-  ( w e. _V -> ( w e. ran ( x e. A |-> B ) <-> E. x e. A w = B ) )
14 13 elv 
 |-  ( w e. ran ( x e. A |-> B ) <-> E. x e. A w = B )
15 14 biimpi 
 |-  ( w e. ran ( x e. A |-> B ) -> E. x e. A w = B )
16 15 adantr 
 |-  ( ( w e. ran ( x e. A |-> B ) /\ y e. w ) -> E. x e. A w = B )
17 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
18 17 nfrn 
 |-  F/_ x ran ( x e. A |-> B )
19 18 nfcri 
 |-  F/ x w e. ran ( x e. A |-> B )
20 nfv 
 |-  F/ x y e. w
21 19 20 nfan 
 |-  F/ x ( w e. ran ( x e. A |-> B ) /\ y e. w )
22 simpl 
 |-  ( ( y e. w /\ w = B ) -> y e. w )
23 simpr 
 |-  ( ( y e. w /\ w = B ) -> w = B )
24 22 23 eleqtrd 
 |-  ( ( y e. w /\ w = B ) -> y e. B )
25 24 ex 
 |-  ( y e. w -> ( w = B -> y e. B ) )
26 25 a1d 
 |-  ( y e. w -> ( x e. A -> ( w = B -> y e. B ) ) )
27 26 adantl 
 |-  ( ( w e. ran ( x e. A |-> B ) /\ y e. w ) -> ( x e. A -> ( w = B -> y e. B ) ) )
28 21 27 reximdai 
 |-  ( ( w e. ran ( x e. A |-> B ) /\ y e. w ) -> ( E. x e. A w = B -> E. x e. A y e. B ) )
29 16 28 mpd 
 |-  ( ( w e. ran ( x e. A |-> B ) /\ y e. w ) -> E. x e. A y e. B )
30 29 ex 
 |-  ( w e. ran ( x e. A |-> B ) -> ( y e. w -> E. x e. A y e. B ) )
31 30 a1i 
 |-  ( y e. U. ran ( x e. A |-> B ) -> ( w e. ran ( x e. A |-> B ) -> ( y e. w -> E. x e. A y e. B ) ) )
32 31 rexlimdv 
 |-  ( y e. U. ran ( x e. A |-> B ) -> ( E. w e. ran ( x e. A |-> B ) y e. w -> E. x e. A y e. B ) )
33 11 32 mpd 
 |-  ( y e. U. ran ( x e. A |-> B ) -> E. x e. A y e. B )
34 9 33 syl 
 |-  ( y e. ( U. ran ( x e. A |-> B ) i^i C ) -> E. x e. A y e. B )
35 34 adantl 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> E. x e. A y e. B )
36 nfv 
 |-  F/ x ph
37 18 nfuni 
 |-  F/_ x U. ran ( x e. A |-> B )
38 nfcv 
 |-  F/_ x C
39 37 38 nfin 
 |-  F/_ x ( U. ran ( x e. A |-> B ) i^i C )
40 39 nfcri 
 |-  F/ x y e. ( U. ran ( x e. A |-> B ) i^i C )
41 36 40 nfan 
 |-  F/ x ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) )
42 nfre1 
 |-  F/ x E. x e. A y e. ( B i^i C )
43 elinel2 
 |-  ( y e. ( U. ran ( x e. A |-> B ) i^i C ) -> y e. C )
44 simp2 
 |-  ( ( y e. C /\ x e. A /\ y e. B ) -> x e. A )
45 simpr 
 |-  ( ( y e. C /\ y e. B ) -> y e. B )
46 simpl 
 |-  ( ( y e. C /\ y e. B ) -> y e. C )
47 45 46 elind 
 |-  ( ( y e. C /\ y e. B ) -> y e. ( B i^i C ) )
48 rspe 
 |-  ( ( x e. A /\ y e. ( B i^i C ) ) -> E. x e. A y e. ( B i^i C ) )
49 44 47 48 3imp3i2an 
 |-  ( ( y e. C /\ x e. A /\ y e. B ) -> E. x e. A y e. ( B i^i C ) )
50 49 3exp 
 |-  ( y e. C -> ( x e. A -> ( y e. B -> E. x e. A y e. ( B i^i C ) ) ) )
51 43 50 syl 
 |-  ( y e. ( U. ran ( x e. A |-> B ) i^i C ) -> ( x e. A -> ( y e. B -> E. x e. A y e. ( B i^i C ) ) ) )
52 51 adantl 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> ( x e. A -> ( y e. B -> E. x e. A y e. ( B i^i C ) ) ) )
53 41 42 52 rexlimd 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> ( E. x e. A y e. B -> E. x e. A y e. ( B i^i C ) ) )
54 35 53 mpd 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> E. x e. A y e. ( B i^i C ) )
55 disjors 
 |-  ( Disj_ x e. A B <-> A. z e. A A. w e. A ( z = w \/ ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) ) )
56 2 55 sylib 
 |-  ( ph -> A. z e. A A. w e. A ( z = w \/ ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) ) )
57 nfv 
 |-  F/ z A. w e. A ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) )
58 nfcv 
 |-  F/_ x A
59 nfv 
 |-  F/ x z = w
60 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
61 nfcv 
 |-  F/_ x w
62 61 nfcsb1 
 |-  F/_ x [_ w / x ]_ B
63 60 62 nfin 
 |-  F/_ x ( [_ z / x ]_ B i^i [_ w / x ]_ B )
64 63 nfeq1 
 |-  F/ x ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/)
65 59 64 nfor 
 |-  F/ x ( z = w \/ ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) )
66 58 65 nfralw 
 |-  F/ x A. w e. A ( z = w \/ ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) )
67 equequ1 
 |-  ( x = z -> ( x = w <-> z = w ) )
68 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
69 68 ineq1d 
 |-  ( x = z -> ( B i^i [_ w / x ]_ B ) = ( [_ z / x ]_ B i^i [_ w / x ]_ B ) )
70 69 eqeq1d 
 |-  ( x = z -> ( ( B i^i [_ w / x ]_ B ) = (/) <-> ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) ) )
71 67 70 orbi12d 
 |-  ( x = z -> ( ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) <-> ( z = w \/ ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) ) ) )
72 71 ralbidv 
 |-  ( x = z -> ( A. w e. A ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) <-> A. w e. A ( z = w \/ ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) ) ) )
73 57 66 72 cbvralw 
 |-  ( A. x e. A A. w e. A ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) <-> A. z e. A A. w e. A ( z = w \/ ( [_ z / x ]_ B i^i [_ w / x ]_ B ) = (/) ) )
74 56 73 sylibr 
 |-  ( ph -> A. x e. A A. w e. A ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) )
75 74 r19.21bi 
 |-  ( ( ph /\ x e. A ) -> A. w e. A ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) )
76 rspa 
 |-  ( ( A. w e. A ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) /\ w e. A ) -> ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) )
77 76 orcomd 
 |-  ( ( A. w e. A ( x = w \/ ( B i^i [_ w / x ]_ B ) = (/) ) /\ w e. A ) -> ( ( B i^i [_ w / x ]_ B ) = (/) \/ x = w ) )
78 75 77 sylan 
 |-  ( ( ( ph /\ x e. A ) /\ w e. A ) -> ( ( B i^i [_ w / x ]_ B ) = (/) \/ x = w ) )
79 elinel1 
 |-  ( y e. ( B i^i C ) -> y e. B )
80 sbsbc 
 |-  ( [ w / x ] y e. ( B i^i C ) <-> [. w / x ]. y e. ( B i^i C ) )
81 sbcel2 
 |-  ( [. w / x ]. y e. ( B i^i C ) <-> y e. [_ w / x ]_ ( B i^i C ) )
82 csbin 
 |-  [_ w / x ]_ ( B i^i C ) = ( [_ w / x ]_ B i^i [_ w / x ]_ C )
83 82 eleq2i 
 |-  ( y e. [_ w / x ]_ ( B i^i C ) <-> y e. ( [_ w / x ]_ B i^i [_ w / x ]_ C ) )
84 80 81 83 3bitri 
 |-  ( [ w / x ] y e. ( B i^i C ) <-> y e. ( [_ w / x ]_ B i^i [_ w / x ]_ C ) )
85 elinel1 
 |-  ( y e. ( [_ w / x ]_ B i^i [_ w / x ]_ C ) -> y e. [_ w / x ]_ B )
86 84 85 sylbi 
 |-  ( [ w / x ] y e. ( B i^i C ) -> y e. [_ w / x ]_ B )
87 inelcm 
 |-  ( ( y e. B /\ y e. [_ w / x ]_ B ) -> ( B i^i [_ w / x ]_ B ) =/= (/) )
88 87 neneqd 
 |-  ( ( y e. B /\ y e. [_ w / x ]_ B ) -> -. ( B i^i [_ w / x ]_ B ) = (/) )
89 79 86 88 syl2an 
 |-  ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> -. ( B i^i [_ w / x ]_ B ) = (/) )
90 pm2.53 
 |-  ( ( ( B i^i [_ w / x ]_ B ) = (/) \/ x = w ) -> ( -. ( B i^i [_ w / x ]_ B ) = (/) -> x = w ) )
91 78 89 90 syl2im 
 |-  ( ( ( ph /\ x e. A ) /\ w e. A ) -> ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) )
92 91 ralrimiva 
 |-  ( ( ph /\ x e. A ) -> A. w e. A ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) )
93 92 ralrimiva 
 |-  ( ph -> A. x e. A A. w e. A ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) )
94 93 adantr 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> A. x e. A A. w e. A ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) )
95 reu2 
 |-  ( E! x e. A y e. ( B i^i C ) <-> ( E. x e. A y e. ( B i^i C ) /\ A. x e. A A. w e. A ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) ) )
96 54 94 95 sylanbrc 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> E! x e. A y e. ( B i^i C ) )
97 riotacl2 
 |-  ( E! x e. A y e. ( B i^i C ) -> ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | y e. ( B i^i C ) } )
98 nfriota1 
 |-  F/_ x ( iota_ x e. A y e. ( B i^i C ) )
99 98 nfcsb1 
 |-  F/_ x [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B
100 99 38 nfin 
 |-  F/_ x ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C )
101 100 nfcri 
 |-  F/ x y e. ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C )
102 csbeq1a 
 |-  ( x = ( iota_ x e. A y e. ( B i^i C ) ) -> B = [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B )
103 102 ineq1d 
 |-  ( x = ( iota_ x e. A y e. ( B i^i C ) ) -> ( B i^i C ) = ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) )
104 103 eleq2d 
 |-  ( x = ( iota_ x e. A y e. ( B i^i C ) ) -> ( y e. ( B i^i C ) <-> y e. ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) ) )
105 98 58 101 104 elrabf 
 |-  ( ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | y e. ( B i^i C ) } <-> ( ( iota_ x e. A y e. ( B i^i C ) ) e. A /\ y e. ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) ) )
106 105 simplbi 
 |-  ( ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | y e. ( B i^i C ) } -> ( iota_ x e. A y e. ( B i^i C ) ) e. A )
107 105 simprbi 
 |-  ( ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | y e. ( B i^i C ) } -> y e. ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) )
108 107 ne0d 
 |-  ( ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | y e. ( B i^i C ) } -> ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) =/= (/) )
109 nfcv 
 |-  F/_ x (/)
110 100 109 nfne 
 |-  F/ x ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) =/= (/)
111 103 neeq1d 
 |-  ( x = ( iota_ x e. A y e. ( B i^i C ) ) -> ( ( B i^i C ) =/= (/) <-> ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) =/= (/) ) )
112 98 58 110 111 elrabf 
 |-  ( ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | ( B i^i C ) =/= (/) } <-> ( ( iota_ x e. A y e. ( B i^i C ) ) e. A /\ ( [_ ( iota_ x e. A y e. ( B i^i C ) ) / x ]_ B i^i C ) =/= (/) ) )
113 106 108 112 sylanbrc 
 |-  ( ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | y e. ( B i^i C ) } -> ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | ( B i^i C ) =/= (/) } )
114 96 97 113 3syl 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | ( B i^i C ) =/= (/) } )
115 114 ralrimiva 
 |-  ( ph -> A. y e. ( U. ran ( x e. A |-> B ) i^i C ) ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | ( B i^i C ) =/= (/) } )
116 62 38 nfin 
 |-  F/_ x ( [_ w / x ]_ B i^i C )
117 116 109 nfne 
 |-  F/ x ( [_ w / x ]_ B i^i C ) =/= (/)
118 csbeq1a 
 |-  ( x = w -> B = [_ w / x ]_ B )
119 118 ineq1d 
 |-  ( x = w -> ( B i^i C ) = ( [_ w / x ]_ B i^i C ) )
120 119 neeq1d 
 |-  ( x = w -> ( ( B i^i C ) =/= (/) <-> ( [_ w / x ]_ B i^i C ) =/= (/) ) )
121 61 58 117 120 elrabf 
 |-  ( w e. { x e. A | ( B i^i C ) =/= (/) } <-> ( w e. A /\ ( [_ w / x ]_ B i^i C ) =/= (/) ) )
122 121 simprbi 
 |-  ( w e. { x e. A | ( B i^i C ) =/= (/) } -> ( [_ w / x ]_ B i^i C ) =/= (/) )
123 n0 
 |-  ( ( [_ w / x ]_ B i^i C ) =/= (/) <-> E. y y e. ( [_ w / x ]_ B i^i C ) )
124 122 123 sylib 
 |-  ( w e. { x e. A | ( B i^i C ) =/= (/) } -> E. y y e. ( [_ w / x ]_ B i^i C ) )
125 124 adantl 
 |-  ( ( ph /\ w e. { x e. A | ( B i^i C ) =/= (/) } ) -> E. y y e. ( [_ w / x ]_ B i^i C ) )
126 121 simplbi 
 |-  ( w e. { x e. A | ( B i^i C ) =/= (/) } -> w e. A )
127 elinel1 
 |-  ( y e. ( [_ w / x ]_ B i^i C ) -> y e. [_ w / x ]_ B )
128 127 adantl 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> y e. [_ w / x ]_ B )
129 simplr 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> w e. A )
130 nfv 
 |-  F/ x ( ph /\ w e. A )
131 62 nfel1 
 |-  F/ x [_ w / x ]_ B e. V
132 130 131 nfim 
 |-  F/ x ( ( ph /\ w e. A ) -> [_ w / x ]_ B e. V )
133 eleq1w 
 |-  ( x = w -> ( x e. A <-> w e. A ) )
134 133 anbi2d 
 |-  ( x = w -> ( ( ph /\ x e. A ) <-> ( ph /\ w e. A ) ) )
135 118 eleq1d 
 |-  ( x = w -> ( B e. V <-> [_ w / x ]_ B e. V ) )
136 134 135 imbi12d 
 |-  ( x = w -> ( ( ( ph /\ x e. A ) -> B e. V ) <-> ( ( ph /\ w e. A ) -> [_ w / x ]_ B e. V ) ) )
137 132 136 1 chvarfv 
 |-  ( ( ph /\ w e. A ) -> [_ w / x ]_ B e. V )
138 137 adantr 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> [_ w / x ]_ B e. V )
139 eqid 
 |-  ( w e. A |-> [_ w / x ]_ B ) = ( w e. A |-> [_ w / x ]_ B )
140 139 elrnmpt1 
 |-  ( ( w e. A /\ [_ w / x ]_ B e. V ) -> [_ w / x ]_ B e. ran ( w e. A |-> [_ w / x ]_ B ) )
141 129 138 140 syl2anc 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> [_ w / x ]_ B e. ran ( w e. A |-> [_ w / x ]_ B ) )
142 nfcv 
 |-  F/_ w B
143 118 equcoms 
 |-  ( w = x -> B = [_ w / x ]_ B )
144 143 eqcomd 
 |-  ( w = x -> [_ w / x ]_ B = B )
145 62 142 144 cbvmpt 
 |-  ( w e. A |-> [_ w / x ]_ B ) = ( x e. A |-> B )
146 145 rneqi 
 |-  ran ( w e. A |-> [_ w / x ]_ B ) = ran ( x e. A |-> B )
147 141 146 eleqtrdi 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> [_ w / x ]_ B e. ran ( x e. A |-> B ) )
148 elunii 
 |-  ( ( y e. [_ w / x ]_ B /\ [_ w / x ]_ B e. ran ( x e. A |-> B ) ) -> y e. U. ran ( x e. A |-> B ) )
149 128 147 148 syl2anc 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> y e. U. ran ( x e. A |-> B ) )
150 elinel2 
 |-  ( y e. ( [_ w / x ]_ B i^i C ) -> y e. C )
151 150 adantl 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> y e. C )
152 149 151 elind 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> y e. ( U. ran ( x e. A |-> B ) i^i C ) )
153 nfv 
 |-  F/ w y e. ( B i^i C )
154 116 nfcri 
 |-  F/ x y e. ( [_ w / x ]_ B i^i C )
155 119 eleq2d 
 |-  ( x = w -> ( y e. ( B i^i C ) <-> y e. ( [_ w / x ]_ B i^i C ) ) )
156 153 154 155 cbvriotaw 
 |-  ( iota_ x e. A y e. ( B i^i C ) ) = ( iota_ w e. A y e. ( [_ w / x ]_ B i^i C ) )
157 simpr 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> y e. ( [_ w / x ]_ B i^i C ) )
158 rspe 
 |-  ( ( w e. A /\ y e. ( [_ w / x ]_ B i^i C ) ) -> E. w e. A y e. ( [_ w / x ]_ B i^i C ) )
159 158 adantll 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> E. w e. A y e. ( [_ w / x ]_ B i^i C ) )
160 simpll 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> ph )
161 sbequ 
 |-  ( w = z -> ( [ w / x ] y e. ( B i^i C ) <-> [ z / x ] y e. ( B i^i C ) ) )
162 sbsbc 
 |-  ( [ z / x ] y e. ( B i^i C ) <-> [. z / x ]. y e. ( B i^i C ) )
163 162 a1i 
 |-  ( w = z -> ( [ z / x ] y e. ( B i^i C ) <-> [. z / x ]. y e. ( B i^i C ) ) )
164 sbcel2 
 |-  ( [. z / x ]. y e. ( B i^i C ) <-> y e. [_ z / x ]_ ( B i^i C ) )
165 csbin 
 |-  [_ z / x ]_ ( B i^i C ) = ( [_ z / x ]_ B i^i [_ z / x ]_ C )
166 csbconstg 
 |-  ( z e. _V -> [_ z / x ]_ C = C )
167 166 elv 
 |-  [_ z / x ]_ C = C
168 167 ineq2i 
 |-  ( [_ z / x ]_ B i^i [_ z / x ]_ C ) = ( [_ z / x ]_ B i^i C )
169 165 168 eqtri 
 |-  [_ z / x ]_ ( B i^i C ) = ( [_ z / x ]_ B i^i C )
170 169 eleq2i 
 |-  ( y e. [_ z / x ]_ ( B i^i C ) <-> y e. ( [_ z / x ]_ B i^i C ) )
171 164 170 bitri 
 |-  ( [. z / x ]. y e. ( B i^i C ) <-> y e. ( [_ z / x ]_ B i^i C ) )
172 171 a1i 
 |-  ( w = z -> ( [. z / x ]. y e. ( B i^i C ) <-> y e. ( [_ z / x ]_ B i^i C ) ) )
173 161 163 172 3bitrd 
 |-  ( w = z -> ( [ w / x ] y e. ( B i^i C ) <-> y e. ( [_ z / x ]_ B i^i C ) ) )
174 173 anbi2d 
 |-  ( w = z -> ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) <-> ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) ) )
175 equequ2 
 |-  ( w = z -> ( x = w <-> x = z ) )
176 174 175 imbi12d 
 |-  ( w = z -> ( ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) <-> ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> x = z ) ) )
177 176 cbvralvw 
 |-  ( A. w e. A ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) <-> A. z e. A ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> x = z ) )
178 177 ralbii 
 |-  ( A. x e. A A. w e. A ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) <-> A. x e. A A. z e. A ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> x = z ) )
179 nfv 
 |-  F/ w A. z e. A ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> x = z )
180 60 38 nfin 
 |-  F/_ x ( [_ z / x ]_ B i^i C )
181 180 nfcri 
 |-  F/ x y e. ( [_ z / x ]_ B i^i C )
182 154 181 nfan 
 |-  F/ x ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) )
183 nfv 
 |-  F/ x w = z
184 182 183 nfim 
 |-  F/ x ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> w = z )
185 58 184 nfralw 
 |-  F/ x A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> w = z )
186 155 anbi1d 
 |-  ( x = w -> ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) <-> ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) ) )
187 equequ1 
 |-  ( x = w -> ( x = z <-> w = z ) )
188 186 187 imbi12d 
 |-  ( x = w -> ( ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> x = z ) <-> ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> w = z ) ) )
189 188 ralbidv 
 |-  ( x = w -> ( A. z e. A ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> x = z ) <-> A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> w = z ) ) )
190 179 185 189 cbvralw 
 |-  ( A. x e. A A. z e. A ( ( y e. ( B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> x = z ) <-> A. w e. A A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> w = z ) )
191 sbsbc 
 |-  ( [ z / w ] y e. ( [_ w / x ]_ B i^i C ) <-> [. z / w ]. y e. ( [_ w / x ]_ B i^i C ) )
192 sbcel2 
 |-  ( [. z / w ]. y e. ( [_ w / x ]_ B i^i C ) <-> y e. [_ z / w ]_ ( [_ w / x ]_ B i^i C ) )
193 csbin 
 |-  [_ z / w ]_ ( [_ w / x ]_ B i^i C ) = ( [_ z / w ]_ [_ w / x ]_ B i^i [_ z / w ]_ C )
194 csbcow 
 |-  [_ z / w ]_ [_ w / x ]_ B = [_ z / x ]_ B
195 csbconstg 
 |-  ( z e. _V -> [_ z / w ]_ C = C )
196 195 elv 
 |-  [_ z / w ]_ C = C
197 194 196 ineq12i 
 |-  ( [_ z / w ]_ [_ w / x ]_ B i^i [_ z / w ]_ C ) = ( [_ z / x ]_ B i^i C )
198 193 197 eqtri 
 |-  [_ z / w ]_ ( [_ w / x ]_ B i^i C ) = ( [_ z / x ]_ B i^i C )
199 198 eleq2i 
 |-  ( y e. [_ z / w ]_ ( [_ w / x ]_ B i^i C ) <-> y e. ( [_ z / x ]_ B i^i C ) )
200 191 192 199 3bitrri 
 |-  ( y e. ( [_ z / x ]_ B i^i C ) <-> [ z / w ] y e. ( [_ w / x ]_ B i^i C ) )
201 200 anbi2i 
 |-  ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) <-> ( y e. ( [_ w / x ]_ B i^i C ) /\ [ z / w ] y e. ( [_ w / x ]_ B i^i C ) ) )
202 201 imbi1i 
 |-  ( ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> w = z ) <-> ( ( y e. ( [_ w / x ]_ B i^i C ) /\ [ z / w ] y e. ( [_ w / x ]_ B i^i C ) ) -> w = z ) )
203 202 2ralbii 
 |-  ( A. w e. A A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ y e. ( [_ z / x ]_ B i^i C ) ) -> w = z ) <-> A. w e. A A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ [ z / w ] y e. ( [_ w / x ]_ B i^i C ) ) -> w = z ) )
204 178 190 203 3bitri 
 |-  ( A. x e. A A. w e. A ( ( y e. ( B i^i C ) /\ [ w / x ] y e. ( B i^i C ) ) -> x = w ) <-> A. w e. A A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ [ z / w ] y e. ( [_ w / x ]_ B i^i C ) ) -> w = z ) )
205 94 204 sylib 
 |-  ( ( ph /\ y e. ( U. ran ( x e. A |-> B ) i^i C ) ) -> A. w e. A A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ [ z / w ] y e. ( [_ w / x ]_ B i^i C ) ) -> w = z ) )
206 160 152 205 syl2anc 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> A. w e. A A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ [ z / w ] y e. ( [_ w / x ]_ B i^i C ) ) -> w = z ) )
207 reu2 
 |-  ( E! w e. A y e. ( [_ w / x ]_ B i^i C ) <-> ( E. w e. A y e. ( [_ w / x ]_ B i^i C ) /\ A. w e. A A. z e. A ( ( y e. ( [_ w / x ]_ B i^i C ) /\ [ z / w ] y e. ( [_ w / x ]_ B i^i C ) ) -> w = z ) ) )
208 159 206 207 sylanbrc 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> E! w e. A y e. ( [_ w / x ]_ B i^i C ) )
209 riota1 
 |-  ( E! w e. A y e. ( [_ w / x ]_ B i^i C ) -> ( ( w e. A /\ y e. ( [_ w / x ]_ B i^i C ) ) <-> ( iota_ w e. A y e. ( [_ w / x ]_ B i^i C ) ) = w ) )
210 208 209 syl 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> ( ( w e. A /\ y e. ( [_ w / x ]_ B i^i C ) ) <-> ( iota_ w e. A y e. ( [_ w / x ]_ B i^i C ) ) = w ) )
211 129 157 210 mpbi2and 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> ( iota_ w e. A y e. ( [_ w / x ]_ B i^i C ) ) = w )
212 156 211 syl5req 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> w = ( iota_ x e. A y e. ( B i^i C ) ) )
213 152 212 jca 
 |-  ( ( ( ph /\ w e. A ) /\ y e. ( [_ w / x ]_ B i^i C ) ) -> ( y e. ( U. ran ( x e. A |-> B ) i^i C ) /\ w = ( iota_ x e. A y e. ( B i^i C ) ) ) )
214 213 ex 
 |-  ( ( ph /\ w e. A ) -> ( y e. ( [_ w / x ]_ B i^i C ) -> ( y e. ( U. ran ( x e. A |-> B ) i^i C ) /\ w = ( iota_ x e. A y e. ( B i^i C ) ) ) ) )
215 126 214 sylan2 
 |-  ( ( ph /\ w e. { x e. A | ( B i^i C ) =/= (/) } ) -> ( y e. ( [_ w / x ]_ B i^i C ) -> ( y e. ( U. ran ( x e. A |-> B ) i^i C ) /\ w = ( iota_ x e. A y e. ( B i^i C ) ) ) ) )
216 215 eximdv 
 |-  ( ( ph /\ w e. { x e. A | ( B i^i C ) =/= (/) } ) -> ( E. y y e. ( [_ w / x ]_ B i^i C ) -> E. y ( y e. ( U. ran ( x e. A |-> B ) i^i C ) /\ w = ( iota_ x e. A y e. ( B i^i C ) ) ) ) )
217 125 216 mpd 
 |-  ( ( ph /\ w e. { x e. A | ( B i^i C ) =/= (/) } ) -> E. y ( y e. ( U. ran ( x e. A |-> B ) i^i C ) /\ w = ( iota_ x e. A y e. ( B i^i C ) ) ) )
218 df-rex 
 |-  ( E. y e. ( U. ran ( x e. A |-> B ) i^i C ) w = ( iota_ x e. A y e. ( B i^i C ) ) <-> E. y ( y e. ( U. ran ( x e. A |-> B ) i^i C ) /\ w = ( iota_ x e. A y e. ( B i^i C ) ) ) )
219 217 218 sylibr 
 |-  ( ( ph /\ w e. { x e. A | ( B i^i C ) =/= (/) } ) -> E. y e. ( U. ran ( x e. A |-> B ) i^i C ) w = ( iota_ x e. A y e. ( B i^i C ) ) )
220 219 ralrimiva 
 |-  ( ph -> A. w e. { x e. A | ( B i^i C ) =/= (/) } E. y e. ( U. ran ( x e. A |-> B ) i^i C ) w = ( iota_ x e. A y e. ( B i^i C ) ) )
221 eqid 
 |-  ( y e. ( U. ran ( x e. A |-> B ) i^i C ) |-> ( iota_ x e. A y e. ( B i^i C ) ) ) = ( y e. ( U. ran ( x e. A |-> B ) i^i C ) |-> ( iota_ x e. A y e. ( B i^i C ) ) )
222 221 fompt 
 |-  ( ( y e. ( U. ran ( x e. A |-> B ) i^i C ) |-> ( iota_ x e. A y e. ( B i^i C ) ) ) : ( U. ran ( x e. A |-> B ) i^i C ) -onto-> { x e. A | ( B i^i C ) =/= (/) } <-> ( A. y e. ( U. ran ( x e. A |-> B ) i^i C ) ( iota_ x e. A y e. ( B i^i C ) ) e. { x e. A | ( B i^i C ) =/= (/) } /\ A. w e. { x e. A | ( B i^i C ) =/= (/) } E. y e. ( U. ran ( x e. A |-> B ) i^i C ) w = ( iota_ x e. A y e. ( B i^i C ) ) ) )
223 115 220 222 sylanbrc 
 |-  ( ph -> ( y e. ( U. ran ( x e. A |-> B ) i^i C ) |-> ( iota_ x e. A y e. ( B i^i C ) ) ) : ( U. ran ( x e. A |-> B ) i^i C ) -onto-> { x e. A | ( B i^i C ) =/= (/) } )
224 fodomg 
 |-  ( ( U. ran ( x e. A |-> B ) i^i C ) e. _V -> ( ( y e. ( U. ran ( x e. A |-> B ) i^i C ) |-> ( iota_ x e. A y e. ( B i^i C ) ) ) : ( U. ran ( x e. A |-> B ) i^i C ) -onto-> { x e. A | ( B i^i C ) =/= (/) } -> { x e. A | ( B i^i C ) =/= (/) } ~<_ ( U. ran ( x e. A |-> B ) i^i C ) ) )
225 8 223 224 sylc 
 |-  ( ph -> { x e. A | ( B i^i C ) =/= (/) } ~<_ ( U. ran ( x e. A |-> B ) i^i C ) )
226 domfi 
 |-  ( ( ( U. ran ( x e. A |-> B ) i^i C ) e. Fin /\ { x e. A | ( B i^i C ) =/= (/) } ~<_ ( U. ran ( x e. A |-> B ) i^i C ) ) -> { x e. A | ( B i^i C ) =/= (/) } e. Fin )
227 6 225 226 syl2anc 
 |-  ( ph -> { x e. A | ( B i^i C ) =/= (/) } e. Fin )