This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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