Theorem trintALT 45324

Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 45324 is an alternate proof of trint 5197. trintALT 45324 is trintALTVD 45323 without virtual deductions and was automatically derived from trintALTVD 45323 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 483	. . . . 5 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦)
2	1	a1i 11	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦))
3		iidn3 44945	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐴)))
4		id 22	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ∀𝑥 ∈ 𝐴 Tr 𝑥)
5		rspsbc 3811	. . . . . . . 8 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
6	3, 4, 5	ee31 45195	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥)))
7		trsbc 44984	. . . . . . . 8 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
8	7	biimpd 230	. . . . . . 7 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
9	3, 6, 8	ee33 44965	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → Tr 𝑞)))
10		simpr 485	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)
11	10	a1i 11	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴))
12		elintg 4885	. . . . . . . . 9 ⊢ (𝑦 ∈ ∩ 𝐴 → (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
13	12	ibi 268	. . . . . . . 8 ⊢ (𝑦 ∈ ∩ 𝐴 → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞)
14	11, 13	syl6 35	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
15		rsp 3227	. . . . . . 7 ⊢ (∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞))
16	14, 15	syl6 35	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)))
17		trel 5187	. . . . . . 7 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
18	17	expd 416	. . . . . 6 ⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞)))
19	9, 2, 16, 18	ee323 44952	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)))
20	19	ralrimdv 3137	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
21		elintg 4885	. . . . 5 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
22	21	biimprd 249	. . . 4 ⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴))
23	2, 20, 22	syl6c 70	. . 3 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
24	23	alrimivv 1935	. 2 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
25		dftr2 5181	. 2 ⊢ (Tr ∩ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
26	24, 25	sylibr 235	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1545   ∈ wcel 2119  ∀wral 3053  [wsbc 3723  ∩ cint 4877  Tr wtr 5179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-v 3433  df-sbc 3724  df-ss 3900  df-uni 4839  df-int 4878  df-tr 5180

This theorem is referenced by: (None)