Theorem trintALT 44870

Description: The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. trintALT 44870 is an alternate proof of trint 5232. trintALT 44870 is trintALTVD 44869 without virtual deductions and was automatically derived from trintALTVD 44869 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 44491	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑞 ∈ 𝐴)))
4		id 22	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ∀𝑥 ∈ 𝐴 Tr 𝑥)
5		rspsbc 3842	. . . . . . . 8 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
6	3, 4, 5	ee31 44741	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥)))
7		trsbc 44530	. . . . . . . 8 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
8	7	biimpd 229	. . . . . . 7 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
9	3, 6, 8	ee33 44511	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → Tr 𝑞)))
10		simpr 484	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)
11	10	a1i 11	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴))
12		elintg 4918	. . . . . . . . 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 5223	. . . . . . 7 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
18	17	expd 415	. . . . . 6 ⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞)))
19	9, 2, 16, 18	ee323 44498	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)))
20	19	ralrimdv 3131	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
21		elintg 4918	. . . . 5 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
22	21	biimprd 248	. . . 4 ⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴))
23	2, 20, 22	syl6c 70	. . 3 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
24	23	alrimivv 1928	. 2 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
25		dftr2 5216	. 2 ⊢ (Tr ∩ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
26	24, 25	sylibr 234	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   ∈ wcel 2109  ∀wral 3044  [wsbc 3753  ∩ cint 4910  Tr wtr 5214

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3449  df-sbc 3754  df-ss 3931  df-uni 4872  df-int 4911  df-tr 5215

This theorem is referenced by: (None)