Theorem trintALTVD 44851

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

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 44584	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   )
2		simpl 482	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦)
3	1, 2	e2 44602	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ 𝑦   )
4		idn3 44586	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑞 ∈ 𝐴   )
5		idn1 44545	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
6		rspsbc 3901	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
7	4, 5, 6	e31 44722	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8		trsbc 44511	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
9	8	biimpd 229	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
10	4, 7, 9	e33 44705	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   Tr 𝑞   )
11		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)
12	1, 11	e2 44602	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑦 ∈ ∩ 𝐴   )
13		elintg 4978	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∩ 𝐴 → (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
14	13	ibi 267	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝐴 → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞)
15	12, 14	e2 44602	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞   )
16		rsp 3253	. . . . . . . . . . . 12 ⊢ (∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞))
17	15, 16	e2 44602	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)   )
18		pm2.27 42	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ((𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞) → 𝑦 ∈ 𝑞))
19	4, 17, 18	e32 44729	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑦 ∈ 𝑞   )
20		trel 5292	. . . . . . . . . . 11 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
21	20	expd 415	. . . . . . . . . 10 ⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞)))
22	10, 3, 19, 21	e323 44737	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑧 ∈ 𝑞   )
23	22	in3 44580	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
24	23	gen21 44590	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
25		df-ral 3068	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 ↔ ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞))
26	25	biimpri 228	. . . . . . 7 ⊢ (∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞)
27	24, 26	e2 44602	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞   )
28		elintg 4978	. . . . . . 7 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
29	28	biimprd 248	. . . . . 6 ⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴))
30	3, 27, 29	e22 44642	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ ∩ 𝐴   )
31	30	in2 44576	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
32	31	gen12 44589	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
33		dftr2 5285	. . . 4 ⊢ (Tr ∩ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
34	33	biimpri 228	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴) → Tr ∩ 𝐴)
35	32, 34	e1a 44598	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∩ 𝐴   )
36	35	in1 44542	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1535   ∈ wcel 2108  ∀wral 3067  [wsbc 3804  ∩ cint 4970  Tr wtr 5283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-v 3490  df-sbc 3805  df-ss 3993  df-uni 4932  df-int 4971  df-tr 5284  df-vd1 44541  df-vd2 44549  df-vd3 44561

This theorem is referenced by: (None)