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∈ATr⁡x→Tr⁡⋃A

Proof

Step Hyp Ref Expression
1 simpr ⊢z∈y∧y∈⋃A→y∈⋃A
2 1 a1i ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→y∈⋃A
3 eluni ⊢y∈⋃A↔∃qy∈q∧q∈A
4 2 3 imbitrdi ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→∃qy∈q∧q∈A
5 simpl ⊢z∈y∧y∈⋃A→z∈y
6 5 a1i ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→z∈y
7 simpl ⊢y∈q∧q∈A→y∈q
8 7 2a1i ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→y∈q∧q∈A→y∈q
9 simpr ⊢y∈q∧q∈A→q∈A
10 9 2a1i ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→y∈q∧q∈A→q∈A
11 rspsbc ⊢q∈A→∀x∈ATr⁡x→[˙q/x]˙Tr⁡x
12 11 com12 ⊢∀x∈ATr⁡x→q∈A→[˙q/x]˙Tr⁡x
13 10 12 syl6d ⊢∀x∈ATr⁡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∈ATr⁡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∈ATr⁡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∈ATr⁡x→z∈y∧y∈⋃A→y∈q∧q∈A→z∈⋃A
23 22 alrimdv ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→∀qy∈q∧q∈A→z∈⋃A
24 19.23v ⊢∀qy∈q∧q∈A→z∈⋃A↔∃qy∈q∧q∈A→z∈⋃A
25 23 24 imbitrdi ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→∃qy∈q∧q∈A→z∈⋃A
26 4 25 mpdd ⊢∀x∈ATr⁡x→z∈y∧y∈⋃A→z∈⋃A
27 26 alrimivv ⊢∀x∈ATr⁡x→∀z∀yz∈y∧y∈⋃A→z∈⋃A
28 dftr2 ⊢Tr⁡⋃A↔∀z∀yz∈y∧y∈⋃A→z∈⋃A
29 27 28 sylibr ⊢∀x∈ATr⁡x→Tr⁡⋃A