Theorem trintALTVD 42389

Description: The intersection of a class of transitive sets is transitive. Virtual deduction proof of trintALT 42390. 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 42390 is trintALTVD 42389 without virtual deductions and was automatically derived from trintALTVD 42389.

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 42122	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   )
2		simpl 482	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦)
3	1, 2	e2 42140	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ 𝑦   )
4		idn3 42124	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑞 ∈ 𝐴   )
5		idn1 42083	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
6		rspsbc 3808	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
7	4, 5, 6	e31 42260	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8		trsbc 42049	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
9	8	biimpd 228	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
10	4, 7, 9	e33 42243	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   Tr 𝑞   )
11		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)
12	1, 11	e2 42140	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑦 ∈ ∩ 𝐴   )
13		elintg 4884	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∩ 𝐴 → (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
14	13	ibi 266	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝐴 → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞)
15	12, 14	e2 42140	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞   )
16		rsp 3129	. . . . . . . . . . . 12 ⊢ (∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞))
17	15, 16	e2 42140	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)   )
18		pm2.27 42	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ((𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞) → 𝑦 ∈ 𝑞))
19	4, 17, 18	e32 42267	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑦 ∈ 𝑞   )
20		trel 5194	. . . . . . . . . . 11 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
21	20	expd 415	. . . . . . . . . 10 ⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞)))
22	10, 3, 19, 21	e323 42275	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑧 ∈ 𝑞   )
23	22	in3 42118	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
24	23	gen21 42128	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
25		df-ral 3068	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 ↔ ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞))
26	25	biimpri 227	. . . . . . 7 ⊢ (∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞)
27	24, 26	e2 42140	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞   )
28		elintg 4884	. . . . . . 7 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
29	28	biimprd 247	. . . . . 6 ⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴))
30	3, 27, 29	e22 42180	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ ∩ 𝐴   )
31	30	in2 42114	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
32	31	gen12 42127	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
33		dftr2 5189	. . . 4 ⊢ (Tr ∩ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
34	33	biimpri 227	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴) → Tr ∩ 𝐴)
35	32, 34	e1a 42136	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∩ 𝐴   )
36	35	in1 42080	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1537   ∈ wcel 2108  ∀wral 3063  [wsbc 3711  ∩ cint 4876  Tr wtr 5187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-v 3424  df-sbc 3712  df-in 3890  df-ss 3900  df-uni 4837  df-int 4877  df-tr 5188  df-vd1 42079  df-vd2 42087  df-vd3 42099

This theorem is referenced by: (None)