Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( z e. y /\ y e. U. A ) -> y e. U. A ) |
2 |
1
|
a1i |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> y e. U. A ) ) |
3 |
|
eluni |
|- ( y e. U. A <-> E. q ( y e. q /\ q e. A ) ) |
4 |
2 3
|
syl6ib |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> E. q ( y e. q /\ q e. A ) ) ) |
5 |
|
simpl |
|- ( ( z e. y /\ y e. U. A ) -> z e. y ) |
6 |
5
|
a1i |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> z e. y ) ) |
7 |
|
simpl |
|- ( ( y e. q /\ q e. A ) -> y e. q ) |
8 |
7
|
2a1i |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> y e. q ) ) ) |
9 |
|
simpr |
|- ( ( y e. q /\ q e. A ) -> q e. A ) |
10 |
9
|
2a1i |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> q e. A ) ) ) |
11 |
|
rspsbc |
|- ( q e. A -> ( A. x e. A Tr x -> [. q / x ]. Tr x ) ) |
12 |
11
|
com12 |
|- ( A. x e. A Tr x -> ( q e. A -> [. q / x ]. Tr x ) ) |
13 |
10 12
|
syl6d |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> [. q / x ]. Tr x ) ) ) |
14 |
|
trsbc |
|- ( q e. A -> ( [. q / x ]. Tr x <-> Tr q ) ) |
15 |
14
|
biimpd |
|- ( q e. A -> ( [. q / x ]. Tr x -> Tr q ) ) |
16 |
10 13 15
|
ee33 |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> Tr q ) ) ) |
17 |
|
trel |
|- ( Tr q -> ( ( z e. y /\ y e. q ) -> z e. q ) ) |
18 |
17
|
expdcom |
|- ( z e. y -> ( y e. q -> ( Tr q -> z e. q ) ) ) |
19 |
6 8 16 18
|
ee233 |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> z e. q ) ) ) |
20 |
|
elunii |
|- ( ( z e. q /\ q e. A ) -> z e. U. A ) |
21 |
20
|
ex |
|- ( z e. q -> ( q e. A -> z e. U. A ) ) |
22 |
19 10 21
|
ee33 |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> z e. U. A ) ) ) |
23 |
22
|
alrimdv |
|- ( 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 ) ) ) |
24 |
|
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 ) ) |
25 |
23 24
|
syl6ib |
|- ( 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 ) ) ) |
26 |
4 25
|
mpdd |
|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ) |
27 |
26
|
alrimivv |
|- ( A. x e. A Tr x -> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ) |
28 |
|
dftr2 |
|- ( Tr U. A <-> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ) |
29 |
27 28
|
sylibr |
|- ( A. x e. A Tr x -> Tr U. A ) |