Theorem trintALT

Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of Enderton p. 73. trintALT is an alternate proof of trint . trintALT is trintALTVD without virtual deductions and was automatically derived from trintALTVD using the tools program translate..without..overwriting.cmd and the Metamath program "MM-PA> MINIMIZE__WITH *" command. (Contributed by Alan Sare, 17-Apr-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	trintALT	|- ( A. x e. A Tr x -> Tr |^| A )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( z e. y /\ y e. |^| A ) -> z e. y )
2	1	a1i	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> z e. y ) )
3		iidn3	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> q e. A ) ) )
4		id	|- ( A. x e. A Tr x -> A. x e. A Tr x )
5		rspsbc	|- ( q e. A -> ( A. x e. A Tr x -> [. q / x ]. Tr x ) )
6	3 4 5	ee31	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> [. q / x ]. Tr x ) ) )
7		trsbc	|- ( q e. A -> ( [. q / x ]. Tr x <-> Tr q ) )
8	7	biimpd	|- ( q e. A -> ( [. q / x ]. Tr x -> Tr q ) )
9	3 6 8	ee33	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> Tr q ) ) )
10		simpr	|- ( ( z e. y /\ y e. |^| A ) -> y e. |^| A )
11	10	a1i	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> y e. |^| A ) )
12		elintg	|- ( y e. |^| A -> ( y e. |^| A <-> A. q e. A y e. q ) )
13	12	ibi	|- ( y e. |^| A -> A. q e. A y e. q )
14	11 13	syl6	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> A. q e. A y e. q ) )
15		rsp	|- ( A. q e. A y e. q -> ( q e. A -> y e. q ) )
16	14 15	syl6	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> y e. q ) ) )
17		trel	|- ( Tr q -> ( ( z e. y /\ y e. q ) -> z e. q ) )
18	17	expd	|- ( Tr q -> ( z e. y -> ( y e. q -> z e. q ) ) )
19	9 2 16 18	ee323	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> ( q e. A -> z e. q ) ) )
20	19	ralrimdv	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> A. q e. A z e. q ) )
21		elintg	|- ( z e. y -> ( z e. |^| A <-> A. q e. A z e. q ) )
22	21	biimprd	|- ( z e. y -> ( A. q e. A z e. q -> z e. |^| A ) )
23	2 20 22	syl6c	|- ( A. x e. A Tr x -> ( ( z e. y /\ y e. |^| A ) -> z e. |^| A ) )
24	23	alrimivv	|- ( A. x e. A Tr x -> A. z A. y ( ( z e. y /\ y e. |^| A ) -> z e. |^| A ) )
25		dftr2	|- ( Tr |^| A <-> A. z A. y ( ( z e. y /\ y e. |^| A ) -> z e. |^| A ) )
26	24 25	sylibr	|- ( A. x e. A Tr x -> Tr |^| A )