Theorem trintALTVD 45235

Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 45236. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. trintALT 45236 is trintALTVD 45235 without virtual deductions and was automatically derived from trintALTVD 45235.

1::	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴Tr 𝑥   )
2::	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   )
3:2:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ 𝑦   )
4:2:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑦 ∈ ∩ 𝐴   )
5:4:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴𝑦 ∈ 𝑞   )
6:5:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)   )
7::	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴), 𝑞 ∈ 𝐴   ▶   𝑞 ∈ 𝐴   )
8:7,6:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴), 𝑞 ∈ 𝐴   ▶   𝑦 ∈ 𝑞   )
9:7,1:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴), 𝑞 ∈ 𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
10:7,9:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴), 𝑞 ∈ 𝐴   ▶   Tr 𝑞   )
11:10,3,8:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴), 𝑞 ∈ 𝐴   ▶   𝑧 ∈ 𝑞   )
12:11:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
13:12:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
14:13:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴𝑧 ∈ 𝑞   )
15:3,14:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ ∩ 𝐴   )
16:15:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
17:16:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
18:17:	⊢ (   ∀𝑥 ∈ 𝐴Tr 𝑥   ▶   Tr ∩ 𝐴   )
qed:18:	⊢ (∀𝑥 ∈ 𝐴Tr 𝑥 → Tr ∩ 𝐴)

(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem trintALTVD

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

Step	Hyp	Ref	Expression
1		idn2 44969	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   )
2		simpl 482	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦)
3	1, 2	e2 44987	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ 𝑦   )
4		idn3 44971	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑞 ∈ 𝐴   )
5		idn1 44930	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
6		rspsbc 3831	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
7	4, 5, 6	e31 45106	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8		trsbc 44896	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
9	8	biimpd 229	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
10	4, 7, 9	e33 45089	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   Tr 𝑞   )
11		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)
12	1, 11	e2 44987	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑦 ∈ ∩ 𝐴   )
13		elintg 4912	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∩ 𝐴 → (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
14	13	ibi 267	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝐴 → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞)
15	12, 14	e2 44987	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞   )
16		rsp 3226	. . . . . . . . . . . 12 ⊢ (∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞))
17	15, 16	e2 44987	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)   )
18		pm2.27 42	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ((𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞) → 𝑦 ∈ 𝑞))
19	4, 17, 18	e32 45113	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑦 ∈ 𝑞   )
20		trel 5215	. . . . . . . . . . 11 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
21	20	expd 415	. . . . . . . . . 10 ⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞)))
22	10, 3, 19, 21	e323 45121	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑧 ∈ 𝑞   )
23	22	in3 44965	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
24	23	gen21 44975	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
25		df-ral 3053	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 ↔ ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞))
26	25	biimpri 228	. . . . . . 7 ⊢ (∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞)
27	24, 26	e2 44987	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞   )
28		elintg 4912	. . . . . . 7 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
29	28	biimprd 248	. . . . . 6 ⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴))
30	3, 27, 29	e22 45027	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ ∩ 𝐴   )
31	30	in2 44961	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
32	31	gen12 44974	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
33		dftr2 5209	. . . 4 ⊢ (Tr ∩ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
34	33	biimpri 228	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴) → Tr ∩ 𝐴)
35	32, 34	e1a 44983	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∩ 𝐴   )
36	35	in1 44927	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3052  [wsbc 3742  ∩ cint 4904  Tr wtr 5207

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-v 3444  df-sbc 3743  df-ss 3920  df-uni 4866  df-int 4905  df-tr 5208  df-vd1 44926  df-vd2 44934  df-vd3 44946

This theorem is referenced by: (None)