Theorem trintALT 45307

Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 45307 is an alternate proof of trint 5210. trintALT 45307 is trintALTVD 45306 without virtual deductions and was automatically derived from trintALTVD 45306 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.)

Assertion

Ref	Expression
trintALT	⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem trintALT

Dummy variables 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 482	. . . . 5 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦)
2	1	a1i 11	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦))
3		iidn3 44928	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐴)))
4		id 22	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ∀𝑥 ∈ 𝐴 Tr 𝑥)
5		rspsbc 3817	. . . . . . . 8 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
6	3, 4, 5	ee31 45178	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥)))
7		trsbc 44967	. . . . . . . 8 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
8	7	biimpd 229	. . . . . . 7 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
9	3, 6, 8	ee33 44948	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → Tr 𝑞)))
10		simpr 484	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)
11	10	a1i 11	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴))
12		elintg 4897	. . . . . . . . 9 ⊢ (𝑦 ∈ ∩ 𝐴 → (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
13	12	ibi 267	. . . . . . . 8 ⊢ (𝑦 ∈ ∩ 𝐴 → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞)
14	11, 13	syl6 35	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
15		rsp 3225	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞))
16	14, 15	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)))
17		trel 5200	. . . . . . 7 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
18	17	expd 415	. . . . . 6 ⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞)))
19	9, 2, 16, 18	ee323 44935	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)))
20	19	ralrimdv 3135	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
21		elintg 4897	. . . . 5 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
22	21	biimprd 248	. . . 4 ⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴))
23	2, 20, 22	syl6c 70	. . 3 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
24	23	alrimivv 1930	. 2 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
25		dftr2 5194	. 2 ⊢ (Tr ∩ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
26	24, 25	sylibr 234	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3051  [wsbc 3728  ∩ cint 4889  Tr wtr 5192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-v 3431  df-sbc 3729  df-ss 3906  df-uni 4851  df-int 4890  df-tr 5193

This theorem is referenced by: (None)