1:: | |- (. A. x e. A Tr x ->. A. x e. A Tr x ).
|
2:: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. ( z e. y /\ y e. |^| A ) ).
|
3:2: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. z e. y ).
|
4:2: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. y e. |^| A ).
|
5:4: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. A. q e. A y e. q ).
|
6:5: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. ( q e. A -> y e. q ) ).
|
7:: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) , q e. A ->. q e. A ).
|
8:7,6: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) , q e. A ->. y e. q ).
|
9:7,1: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) , q e. A ->. [ q / x ] Tr x ).
|
10:7,9: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) , q e. A ->. Tr q ).
|
11:10,3,8: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) , q e. A ->. z e. q ).
|
12:11: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. ( q e. A -> z e. q ) ).
|
13:12: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. A. q ( q e. A -> z e. q ) ).
|
14:13: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. A. q e. A z e. q ).
|
15:3,14: | |- (. A. x e. A Tr x ,. ( z e. y /\ y e.
|^| A ) ->. z e. |^| A ).
|
16:15: | |- (. A. x e. A Tr x ->. ( ( z e. y /\ y
e. |^| A ) -> z e. |^| A ) ).
|
17:16: | |- (. A. x e. A Tr x ->. A. z A. y ( ( z
e. y /\ y e. |^| A ) -> z e. |^| A ) ).
|
18:17: | |- (. A. x e. A Tr x ->. Tr |^| A ).
|
qed:18: | |- ( A. x e. A Tr x -> Tr |^| A )
|