Theorem truniALTVD 45237

Description: The union of a class of transitive sets is transitive. 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. truniALT 44901 is truniALTVD 45237 without virtual deductions and was automatically derived from truniALTVD 45237.

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

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

Assertion

Ref	Expression
truniALTVD	⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

Distinct variable group:   𝑥,𝐴

Proof of Theorem truniALTVD

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

Step	Hyp	Ref	Expression
1		idn2 44973	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   )
2		simpr 484	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴)
3	1, 2	e2 44991	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑦 ∈ ∪ 𝐴   )
4		eluni 4868	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
5	4	biimpi 216	. . . . . . 7 ⊢ (𝑦 ∈ ∪ 𝐴 → ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
6	3, 5	e2 44991	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
7		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦)
8	1, 7	e2 44991	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ 𝑦   )
9		idn3 44975	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
10		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞)
11	9, 10	e3 45096	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑦 ∈ 𝑞   )
12		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)
13	9, 12	e3 45096	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑞 ∈ 𝐴   )
14		idn1 44934	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
15		rspsbc 3831	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
16	15	com12 32	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥))
17	14, 13, 16	e13 45107	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18		trsbc 44900	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
19	18	biimpd 229	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
20	13, 17, 19	e33 45093	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   Tr 𝑞   )
21		trel 5215	. . . . . . . . . . . 12 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
22	21	expdcom 414	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → (Tr 𝑞 → 𝑧 ∈ 𝑞)))
23	8, 11, 20, 22	e233 45124	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ 𝑞   )
24		elunii 4870	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)
25	24	ex 412	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴))
26	23, 13, 25	e33 45093	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
27	26	in3 44969	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
28	27	gen21 44979	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
29		19.23v 1944	. . . . . . . 8 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ↔ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
30	29	biimpi 216	. . . . . . 7 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
31	28, 30	e2 44991	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
32		pm2.27 42	. . . . . 6 ⊢ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → ((∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
33	6, 31, 32	e22 45031	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
34	33	in2 44965	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
35	34	gen12 44978	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
36		dftr2 5209	. . . 4 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
37	36	biimpri 228	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) → Tr ∪ 𝐴)
38	35, 37	e1a 44987	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∪ 𝐴   )
39	38	in1 44931	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1540  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  [wsbc 3742  ∪ cuni 4865  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-tr 5208  df-vd1 44930  df-vd2 44938  df-vd3 44950

This theorem is referenced by: (None)