Theorem truniALTVD 46049

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 45713 is truniALTVD 46049 without virtual deductions and was automatically derived from truniALTVD 46049.

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 45785	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   )
2		simpr 490	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴)
3	1, 2	e2 45803	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑦 ∈ ∪ 𝐴   )
4		eluni 4873	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
5	4	biimpi 219	. . . . . . 7 ⊢ (𝑦 ∈ ∪ 𝐴 → ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
6	3, 5	e2 45803	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
7		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦)
8	1, 7	e2 45803	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ 𝑦   )
9		idn3 45787	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
10		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞)
11	9, 10	e3 45908	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑦 ∈ 𝑞   )
12		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)
13	9, 12	e3 45908	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑞 ∈ 𝐴   )
14		idn1 45746	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
15		rspsbc 3830	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
16	15	com12 33	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥))
17	14, 13, 16	e13 45919	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18		trsbc 45712	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
19	18	biimpd 232	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
20	13, 17, 19	e33 45905	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   Tr 𝑞   )
21		trel 5223	. . . . . . . . . . . 12 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
22	21	expdcom 420	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → (Tr 𝑞 → 𝑧 ∈ 𝑞)))
23	8, 11, 20, 22	e233 45936	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ 𝑞   )
24		elunii 4875	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)
25	24	ex 418	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴))
26	23, 13, 25	e33 45905	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
27	26	in3 45781	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
28	27	gen21 45791	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
29		19.23v 1977	. . . . . . . 8 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ↔ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
30	29	biimpi 219	. . . . . . 7 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
31	28, 30	e2 45803	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
32		pm2.27 43	. . . . . 6 ⊢ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → ((∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
33	6, 31, 32	e22 45843	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
34	33	in2 45777	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
35	34	gen12 45790	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
36		dftr2 5217	. . . 4 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
37	36	biimpri 231	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) → Tr ∪ 𝐴)
38	35, 37	e1a 45799	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∪ 𝐴   )
39	38	in1 45743	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2147  ∀wral 3080  [wsbc 3742  ∪ cuni 4870  Tr wtr 5215

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-v 3456  df-sbc 3743  df-ss 3901  df-uni 4871  df-tr 5216  df-vd1 45742  df-vd2 45750  df-vd3 45762

This theorem is used by: (None)