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 ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑧 ∈ 𝑦 )
2 1 a1i ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑧 ∈ 𝑦 ) )
3 iidn3 ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → ( 𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐴 ) ) )
4 id ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ∀ 𝑥 ∈ 𝐴 Tr 𝑥 )
5 rspsbc ⊢ ( 𝑞 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → [ 𝑞 / 𝑥 ] Tr 𝑥 ) )
6 3 4 5 ee31 ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → ( 𝑞 ∈ 𝐴 → [ 𝑞 / 𝑥 ] Tr 𝑥 ) ) )
7 trsbc ⊢ ( 𝑞 ∈ 𝐴 → ( [ 𝑞 / 𝑥 ] Tr 𝑥 ↔ Tr 𝑞 ) )
8 7 biimpd ⊢ ( 𝑞 ∈ 𝐴 → ( [ 𝑞 / 𝑥 ] Tr 𝑥 → Tr 𝑞 ) )
9 3 6 8 ee33 ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → ( 𝑞 ∈ 𝐴 → Tr 𝑞 ) ) )
10 simpr ⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑦 ∈ ∩ 𝐴 )
11 10 a1i ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑦 ∈ ∩ 𝐴 ) )
12 elintg ⊢ ( 𝑦 ∈ ∩ 𝐴 → ( 𝑦 ∈ ∩ 𝐴 ↔ ∀ 𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 ) )
13 12 ibi ⊢ ( 𝑦 ∈ ∩ 𝐴 → ∀ 𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 )
14 11 13 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → ∀ 𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 ) )
15 rsp ⊢ ( ∀ 𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 → ( 𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞 ) )
16 14 15 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → ( 𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞 ) ) )
17 trel ⊢ ( Tr 𝑞 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞 ) → 𝑧 ∈ 𝑞 ) )
18 17 expd ⊢ ( Tr 𝑞 → ( 𝑧 ∈ 𝑦 → ( 𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞 ) ) )
19 9 2 16 18 ee323 ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → ( 𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞 ) ) )
20 19 ralrimdv ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → ∀ 𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 ) )
21 elintg ⊢ ( 𝑧 ∈ 𝑦 → ( 𝑧 ∈ ∩ 𝐴 ↔ ∀ 𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 ) )
22 21 biimprd ⊢ ( 𝑧 ∈ 𝑦 → ( ∀ 𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴 ) )
23 2 20 22 syl6c ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑧 ∈ ∩ 𝐴 ) )
24 23 alrimivv ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑧 ∈ ∩ 𝐴 ) )
25 dftr2 ⊢ ( Tr ∩ 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑧 ∈ ∩ 𝐴 ) )
26 24 25 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴 )