Metamath Proof Explorer

Theorem disjinfi

Description: Only a finite number of disjoint sets can have a nonempty intersection with a finite set C . The proof uses fodomfi rather than fodomg , and so does not require ax-ac . (Contributed by Glauco Siliprandi, 17-Aug-2020) (Revised by Vincent Gonzalez, 19-Aug-2026)

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