Metamath Proof Explorer

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 ⊢∀x∈ATr⁡x→Tr⁡⋂A

Proof

Step Hyp Ref Expression
1 simpl ⊢z∈y∧y∈⋂A→z∈y
2 1 a1i ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→z∈y
3 iidn3 ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→q∈A→q∈A
4 id ⊢∀x∈ATr⁡x→∀x∈ATr⁡x
5 rspsbc ⊢q∈A→∀x∈ATr⁡x→[˙q/x]˙Tr⁡x
6 3 4 5 ee31 ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→q∈A→[˙q/x]˙Tr⁡x
7 trsbc ⊢q∈A→[˙q/x]˙Tr⁡x↔Tr⁡q
8 7 biimpd ⊢q∈A→[˙q/x]˙Tr⁡x→Tr⁡q
9 3 6 8 ee33 ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→q∈A→Tr⁡q
10 simpr ⊢z∈y∧y∈⋂A→y∈⋂A
11 10 a1i ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→y∈⋂A
12 elintg ⊢y∈⋂A→y∈⋂A↔∀q∈Ay∈q
13 12 ibi ⊢y∈⋂A→∀q∈Ay∈q
14 11 13 syl6 ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→∀q∈Ay∈q
15 rsp ⊢∀q∈Ay∈q→q∈A→y∈q
16 14 15 syl6 ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→q∈A→y∈q
17 trel ⊢Tr⁡q→z∈y∧y∈q→z∈q
18 17 expd ⊢Tr⁡q→z∈y→y∈q→z∈q
19 9 2 16 18 ee323 ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→q∈A→z∈q
20 19 ralrimdv ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→∀q∈Az∈q
21 elintg ⊢z∈y→z∈⋂A↔∀q∈Az∈q
22 21 biimprd ⊢z∈y→∀q∈Az∈q→z∈⋂A
23 2 20 22 syl6c ⊢∀x∈ATr⁡x→z∈y∧y∈⋂A→z∈⋂A
24 23 alrimivv ⊢∀x∈ATr⁡x→∀z∀yz∈y∧y∈⋂A→z∈⋂A
25 dftr2 ⊢Tr⁡⋂A↔∀z∀yz∈y∧y∈⋂A→z∈⋂A
26 24 25 sylibr ⊢∀x∈ATr⁡x→Tr⁡⋂A