Step |
Hyp |
Ref |
Expression |
1 |
|
idn2 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( z e. y /\ y e. U. A ) ). |
2 |
|
simpr |
|- ( ( z e. y /\ y e. U. A ) -> y e. U. A ) |
3 |
1 2
|
e2 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. y e. U. A ). |
4 |
|
eluni |
|- ( y e. U. A <-> E. q ( y e. q /\ q e. A ) ) |
5 |
4
|
biimpi |
|- ( y e. U. A -> E. q ( y e. q /\ q e. A ) ) |
6 |
3 5
|
e2 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. E. q ( y e. q /\ q e. A ) ). |
7 |
|
simpl |
|- ( ( z e. y /\ y e. U. A ) -> z e. y ) |
8 |
1 7
|
e2 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. z e. y ). |
9 |
|
idn3 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. ( y e. q /\ q e. A ) ). |
10 |
|
simpl |
|- ( ( y e. q /\ q e. A ) -> y e. q ) |
11 |
9 10
|
e3 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. y e. q ). |
12 |
|
simpr |
|- ( ( y e. q /\ q e. A ) -> q e. A ) |
13 |
9 12
|
e3 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. q e. A ). |
14 |
|
idn1 |
|- (. A. x e. A Tr x ->. A. x e. A Tr x ). |
15 |
|
rspsbc |
|- ( q e. A -> ( A. x e. A Tr x -> [. q / x ]. Tr x ) ) |
16 |
15
|
com12 |
|- ( A. x e. A Tr x -> ( q e. A -> [. q / x ]. Tr x ) ) |
17 |
14 13 16
|
e13 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. [. q / x ]. Tr x ). |
18 |
|
trsbc |
|- ( q e. A -> ( [. q / x ]. Tr x <-> Tr q ) ) |
19 |
18
|
biimpd |
|- ( q e. A -> ( [. q / x ]. Tr x -> Tr q ) ) |
20 |
13 17 19
|
e33 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. Tr q ). |
21 |
|
trel |
|- ( Tr q -> ( ( z e. y /\ y e. q ) -> z e. q ) ) |
22 |
21
|
expdcom |
|- ( z e. y -> ( y e. q -> ( Tr q -> z e. q ) ) ) |
23 |
8 11 20 22
|
e233 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. z e. q ). |
24 |
|
elunii |
|- ( ( z e. q /\ q e. A ) -> z e. U. A ) |
25 |
24
|
ex |
|- ( z e. q -> ( q e. A -> z e. U. A ) ) |
26 |
23 13 25
|
e33 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ,. ( y e. q /\ q e. A ) ->. z e. U. A ). |
27 |
26
|
in3 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( ( y e. q /\ q e. A ) -> z e. U. A ) ). |
28 |
27
|
gen21 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. A. q ( ( y e. q /\ q e. A ) -> z e. U. A ) ). |
29 |
|
19.23v |
|- ( A. q ( ( y e. q /\ q e. A ) -> z e. U. A ) <-> ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) ) |
30 |
29
|
biimpi |
|- ( A. q ( ( y e. q /\ q e. A ) -> z e. U. A ) -> ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) ) |
31 |
28 30
|
e2 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) ). |
32 |
|
pm2.27 |
|- ( E. q ( y e. q /\ q e. A ) -> ( ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) -> z e. U. A ) ) |
33 |
6 31 32
|
e22 |
|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. z e. U. A ). |
34 |
33
|
in2 |
|- (. A. x e. A Tr x ->. ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ). |
35 |
34
|
gen12 |
|- (. A. x e. A Tr x ->. A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ). |
36 |
|
dftr2 |
|- ( Tr U. A <-> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ) |
37 |
36
|
biimpri |
|- ( A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) -> Tr U. A ) |
38 |
35 37
|
e1a |
|- (. A. x e. A Tr x ->. Tr U. A ). |
39 |
38
|
in1 |
|- ( A. x e. A Tr x -> Tr U. A ) |