Metamath Proof Explorer


Theorem truniALT

Description: The union of a class of transitive sets is transitive. Alternate proof of truni . truniALT is truniALTVD without virtual deductions and was automatically derived from truniALTVD using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion truniALT x A Tr x Tr A

Proof

Step Hyp Ref Expression
1 simpr z y y A y A
2 1 a1i x A Tr x z y y A y A
3 eluni y A q y q q A
4 2 3 syl6ib x A Tr x z y y A q y q q A
5 simpl z y y A z y
6 5 a1i x A Tr x z y y A z y
7 simpl y q q A y q
8 7 2a1i x A Tr x z y y A y q q A y q
9 simpr y q q A q A
10 9 2a1i x A Tr x z y y A y q q A q A
11 rspsbc q A x A Tr x [˙q / x]˙ Tr x
12 11 com12 x A Tr x q A [˙q / x]˙ Tr x
13 10 12 syl6d x A Tr x z y y A y q q A [˙q / x]˙ Tr x
14 trsbc q A [˙q / x]˙ Tr x Tr q
15 14 biimpd q A [˙q / x]˙ Tr x Tr q
16 10 13 15 ee33 x A Tr x z y y A y q q A Tr q
17 trel Tr q z y y q z q
18 17 expdcom z y y q Tr q z q
19 6 8 16 18 ee233 x A Tr x z y y A y q q A z q
20 elunii z q q A z A
21 20 ex z q q A z A
22 19 10 21 ee33 x A Tr x z y y A y q q A z A
23 22 alrimdv x A Tr x z y y A q y q q A z A
24 19.23v q y q q A z A q y q q A z A
25 23 24 syl6ib x A Tr x z y y A q y q q A z A
26 4 25 mpdd x A Tr x z y y A z A
27 26 alrimivv x A Tr x z y z y y A z A
28 dftr2 Tr A z y z y y A z A
29 27 28 sylibr x A Tr x Tr A