Metamath Proof Explorer


Theorem trintALTVD

Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trintALT is trintALTVD without virtual deductions and was automatically derived from trintALTVD .

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 )
(Contributed by Alan Sare, 17-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion trintALTVD xATrxTrA

Proof

Step Hyp Ref Expression
1 idn2 xATrx,zyyAzyyA
2 simpl zyyAzy
3 1 2 e2 xATrx,zyyAzy
4 idn3 xATrx,zyyA,qAqA
5 idn1 xATrxxATrx
6 rspsbc qAxATrx[˙q/x]˙Trx
7 4 5 6 e31 xATrx,zyyA,qA[˙q/x]˙Trx
8 trsbc qA[˙q/x]˙TrxTrq
9 8 biimpd qA[˙q/x]˙TrxTrq
10 4 7 9 e33 xATrx,zyyA,qATrq
11 simpr zyyAyA
12 1 11 e2 xATrx,zyyAyA
13 elintg yAyAqAyq
14 13 ibi yAqAyq
15 12 14 e2 xATrx,zyyAqAyq
16 rsp qAyqqAyq
17 15 16 e2 xATrx,zyyAqAyq
18 pm2.27 qAqAyqyq
19 4 17 18 e32 xATrx,zyyA,qAyq
20 trel Trqzyyqzq
21 20 expd Trqzyyqzq
22 10 3 19 21 e323 xATrx,zyyA,qAzq
23 22 in3 xATrx,zyyAqAzq
24 23 gen21 xATrx,zyyAqqAzq
25 df-ral qAzqqqAzq
26 25 biimpri qqAzqqAzq
27 24 26 e2 xATrx,zyyAqAzq
28 elintg zyzAqAzq
29 28 biimprd zyqAzqzA
30 3 27 29 e22 xATrx,zyyAzA
31 30 in2 xATrxzyyAzA
32 31 gen12 xATrxzyzyyAzA
33 dftr2 TrAzyzyyAzA
34 33 biimpri zyzyyAzATrA
35 32 34 e1a xATrxTrA
36 35 in1 xATrxTrA