Theorem trintALTVD 43641

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

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 43374	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   )
2		simpl 484	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ 𝑦)
3	1, 2	e2 43392	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ 𝑦   )
4		idn3 43376	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑞 ∈ 𝐴   )
5		idn1 43335	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
6		rspsbc 3874	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
7	4, 5, 6	e31 43512	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   [𝑞 / 𝑥]Tr 𝑥   )
8		trsbc 43301	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
9	8	biimpd 228	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
10	4, 7, 9	e33 43495	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   Tr 𝑞   )
11		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑦 ∈ ∩ 𝐴)
12	1, 11	e2 43392	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑦 ∈ ∩ 𝐴   )
13		elintg 4959	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∩ 𝐴 → (𝑦 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞))
14	13	ibi 267	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ∩ 𝐴 → ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞)
15	12, 14	e2 43392	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞   )
16		rsp 3245	. . . . . . . . . . . 12 ⊢ (∀𝑞 ∈ 𝐴 𝑦 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞))
17	15, 16	e2 43392	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞)   )
18		pm2.27 42	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → ((𝑞 ∈ 𝐴 → 𝑦 ∈ 𝑞) → 𝑦 ∈ 𝑞))
19	4, 17, 18	e32 43519	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑦 ∈ 𝑞   )
20		trel 5275	. . . . . . . . . . 11 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
21	20	expd 417	. . . . . . . . . 10 ⊢ (Tr 𝑞 → (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → 𝑧 ∈ 𝑞)))
22	10, 3, 19, 21	e323 43527	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ,   𝑞 ∈ 𝐴   ▶   𝑧 ∈ 𝑞   )
23	22	in3 43370	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   (𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
24	23	gen21 43380	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞)   )
25		df-ral 3063	. . . . . . . 8 ⊢ (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 ↔ ∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞))
26	25	biimpri 227	. . . . . . 7 ⊢ (∀𝑞(𝑞 ∈ 𝐴 → 𝑧 ∈ 𝑞) → ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞)
27	24, 26	e2 43392	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞   )
28		elintg 4959	. . . . . . 7 ⊢ (𝑧 ∈ 𝑦 → (𝑧 ∈ ∩ 𝐴 ↔ ∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞))
29	28	biimprd 247	. . . . . 6 ⊢ (𝑧 ∈ 𝑦 → (∀𝑞 ∈ 𝐴 𝑧 ∈ 𝑞 → 𝑧 ∈ ∩ 𝐴))
30	3, 27, 29	e22 43432	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴)   ▶   𝑧 ∈ ∩ 𝐴   )
31	30	in2 43366	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
32	31	gen12 43379	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴)   )
33		dftr2 5268	. . . 4 ⊢ (Tr ∩ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴))
34	33	biimpri 227	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∩ 𝐴) → 𝑧 ∈ ∩ 𝐴) → Tr ∩ 𝐴)
35	32, 34	e1a 43388	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∩ 𝐴   )
36	35	in1 43332	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∩ 𝐴)

Syntax hints:   → wi 4   ∧ wa 397  ∀wal 1540   ∈ wcel 2107  ∀wral 3062  [wsbc 3778  ∩ cint 4951  Tr wtr 5266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-v 3477  df-sbc 3779  df-in 3956  df-ss 3966  df-uni 4910  df-int 4952  df-tr 5267  df-vd1 43331  df-vd2 43339  df-vd3 43351

This theorem is referenced by: (None)