Step |
Hyp |
Ref |
Expression |
1 |
|
disjf1.xph |
|- F/ x ph |
2 |
|
disjf1.f |
|- F = ( x e. A |-> B ) |
3 |
|
disjf1.b |
|- ( ( ph /\ x e. A ) -> B e. V ) |
4 |
|
disjf1.n0 |
|- ( ( ph /\ x e. A ) -> B =/= (/) ) |
5 |
|
disjf1.dj |
|- ( ph -> Disj_ x e. A B ) |
6 |
|
nfv |
|- F/ x y e. A |
7 |
1 6
|
nfan |
|- F/ x ( ph /\ y e. A ) |
8 |
|
nfcsb1v |
|- F/_ x [_ y / x ]_ B |
9 |
|
nfcv |
|- F/_ x V |
10 |
8 9
|
nfel |
|- F/ x [_ y / x ]_ B e. V |
11 |
7 10
|
nfim |
|- F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. V ) |
12 |
|
eleq1w |
|- ( x = y -> ( x e. A <-> y e. A ) ) |
13 |
12
|
anbi2d |
|- ( x = y -> ( ( ph /\ x e. A ) <-> ( ph /\ y e. A ) ) ) |
14 |
|
csbeq1a |
|- ( x = y -> B = [_ y / x ]_ B ) |
15 |
14
|
eleq1d |
|- ( x = y -> ( B e. V <-> [_ y / x ]_ B e. V ) ) |
16 |
13 15
|
imbi12d |
|- ( x = y -> ( ( ( ph /\ x e. A ) -> B e. V ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. V ) ) ) |
17 |
11 16 3
|
chvarfv |
|- ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. V ) |
18 |
17
|
ralrimiva |
|- ( ph -> A. y e. A [_ y / x ]_ B e. V ) |
19 |
|
inidm |
|- ( [_ y / x ]_ B i^i [_ y / x ]_ B ) = [_ y / x ]_ B |
20 |
19
|
eqcomi |
|- [_ y / x ]_ B = ( [_ y / x ]_ B i^i [_ y / x ]_ B ) |
21 |
20
|
a1i |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> [_ y / x ]_ B = ( [_ y / x ]_ B i^i [_ y / x ]_ B ) ) |
22 |
|
ineq2 |
|- ( [_ y / x ]_ B = [_ z / x ]_ B -> ( [_ y / x ]_ B i^i [_ y / x ]_ B ) = ( [_ y / x ]_ B i^i [_ z / x ]_ B ) ) |
23 |
22
|
ad2antlr |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> ( [_ y / x ]_ B i^i [_ y / x ]_ B ) = ( [_ y / x ]_ B i^i [_ z / x ]_ B ) ) |
24 |
|
nfcv |
|- F/_ w B |
25 |
|
nfcsb1v |
|- F/_ x [_ w / x ]_ B |
26 |
|
csbeq1a |
|- ( x = w -> B = [_ w / x ]_ B ) |
27 |
24 25 26
|
cbvdisj |
|- ( Disj_ x e. A B <-> Disj_ w e. A [_ w / x ]_ B ) |
28 |
5 27
|
sylib |
|- ( ph -> Disj_ w e. A [_ w / x ]_ B ) |
29 |
28
|
ad3antrrr |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> Disj_ w e. A [_ w / x ]_ B ) |
30 |
|
simpllr |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> ( y e. A /\ z e. A ) ) |
31 |
|
neqne |
|- ( -. y = z -> y =/= z ) |
32 |
31
|
adantl |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> y =/= z ) |
33 |
|
csbeq1 |
|- ( w = y -> [_ w / x ]_ B = [_ y / x ]_ B ) |
34 |
|
csbeq1 |
|- ( w = z -> [_ w / x ]_ B = [_ z / x ]_ B ) |
35 |
33 34
|
disji2 |
|- ( ( Disj_ w e. A [_ w / x ]_ B /\ ( y e. A /\ z e. A ) /\ y =/= z ) -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) |
36 |
29 30 32 35
|
syl3anc |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) |
37 |
21 23 36
|
3eqtrd |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> [_ y / x ]_ B = (/) ) |
38 |
|
nfcv |
|- F/_ x (/) |
39 |
8 38
|
nfne |
|- F/ x [_ y / x ]_ B =/= (/) |
40 |
7 39
|
nfim |
|- F/ x ( ( ph /\ y e. A ) -> [_ y / x ]_ B =/= (/) ) |
41 |
14
|
neeq1d |
|- ( x = y -> ( B =/= (/) <-> [_ y / x ]_ B =/= (/) ) ) |
42 |
13 41
|
imbi12d |
|- ( x = y -> ( ( ( ph /\ x e. A ) -> B =/= (/) ) <-> ( ( ph /\ y e. A ) -> [_ y / x ]_ B =/= (/) ) ) ) |
43 |
40 42 4
|
chvarfv |
|- ( ( ph /\ y e. A ) -> [_ y / x ]_ B =/= (/) ) |
44 |
43
|
adantrr |
|- ( ( ph /\ ( y e. A /\ z e. A ) ) -> [_ y / x ]_ B =/= (/) ) |
45 |
44
|
ad2antrr |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> [_ y / x ]_ B =/= (/) ) |
46 |
45
|
neneqd |
|- ( ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) /\ -. y = z ) -> -. [_ y / x ]_ B = (/) ) |
47 |
37 46
|
condan |
|- ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ [_ y / x ]_ B = [_ z / x ]_ B ) -> y = z ) |
48 |
47
|
ex |
|- ( ( ph /\ ( y e. A /\ z e. A ) ) -> ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) ) |
49 |
48
|
ralrimivva |
|- ( ph -> A. y e. A A. z e. A ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) ) |
50 |
18 49
|
jca |
|- ( ph -> ( A. y e. A [_ y / x ]_ B e. V /\ A. y e. A A. z e. A ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) ) ) |
51 |
|
nfcv |
|- F/_ y B |
52 |
51 8 14
|
cbvmpt |
|- ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B ) |
53 |
2 52
|
eqtri |
|- F = ( y e. A |-> [_ y / x ]_ B ) |
54 |
|
csbeq1 |
|- ( y = z -> [_ y / x ]_ B = [_ z / x ]_ B ) |
55 |
53 54
|
f1mpt |
|- ( F : A -1-1-> V <-> ( A. y e. A [_ y / x ]_ B e. V /\ A. y e. A A. z e. A ( [_ y / x ]_ B = [_ z / x ]_ B -> y = z ) ) ) |
56 |
50 55
|
sylibr |
|- ( ph -> F : A -1-1-> V ) |