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

Proof

Step Hyp Ref Expression
1 simpl ⊢ z ∈ y ∧ y ∈ ⋂ A → z ∈ y
2 1 a1i ⊢ ∀ x ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → z ∈ y
3 iidn3 ⊢ ∀ x ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → q ∈ A → q ∈ A
4 id ⊢ ∀ x ∈ A Tr ⁡ x → ∀ x ∈ A Tr ⁡ x
5 rspsbc ⊢ q ∈ A → ∀ x ∈ A Tr ⁡ x → [˙q / x]˙ Tr ⁡ x
6 3 4 5 ee31 ⊢ ∀ x ∈ A Tr ⁡ 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 ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → q ∈ A → Tr ⁡ q
10 simpr ⊢ z ∈ y ∧ y ∈ ⋂ A → y ∈ ⋂ A
11 10 a1i ⊢ ∀ x ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → y ∈ ⋂ A
12 elintg ⊢ y ∈ ⋂ A → y ∈ ⋂ A ↔ ∀ q ∈ A y ∈ q
13 12 ibi ⊢ y ∈ ⋂ A → ∀ q ∈ A y ∈ q
14 11 13 syl6 ⊢ ∀ x ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → ∀ q ∈ A y ∈ q
15 rsp ⊢ ∀ q ∈ A y ∈ q → q ∈ A → y ∈ q
16 14 15 syl6 ⊢ ∀ x ∈ A Tr ⁡ 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 ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → q ∈ A → z ∈ q
20 19 ralrimdv ⊢ ∀ x ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → ∀ q ∈ A z ∈ q
21 elintg ⊢ z ∈ y → z ∈ ⋂ A ↔ ∀ q ∈ A z ∈ q
22 21 biimprd ⊢ z ∈ y → ∀ q ∈ A z ∈ q → z ∈ ⋂ A
23 2 20 22 syl6c ⊢ ∀ x ∈ A Tr ⁡ x → z ∈ y ∧ y ∈ ⋂ A → z ∈ ⋂ A
24 23 alrimivv ⊢ ∀ x ∈ A Tr ⁡ x → ∀ z ∀ y z ∈ y ∧ y ∈ ⋂ A → z ∈ ⋂ A
25 dftr2 ⊢ Tr ⁡ ⋂ A ↔ ∀ z ∀ y z ∈ y ∧ y ∈ ⋂ A → z ∈ ⋂ A
26 24 25 sylibr ⊢ ∀ x ∈ A Tr ⁡ x → Tr ⁡ ⋂ A