Theorem truniALTVD 45664

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

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 45400	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   )
2		simpr 490	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴)
3	1, 2	e2 45418	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑦 ∈ ∪ 𝐴   )
4		eluni 4877	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
5	4	biimpi 219	. . . . . . 7 ⊢ (𝑦 ∈ ∪ 𝐴 → ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
6	3, 5	e2 45418	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
7		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦)
8	1, 7	e2 45418	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ 𝑦   )
9		idn3 45402	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
10		simpl 488	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞)
11	9, 10	e3 45523	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑦 ∈ 𝑞   )
12		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)
13	9, 12	e3 45523	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑞 ∈ 𝐴   )
14		idn1 45361	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
15		rspsbc 3833	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
16	15	com12 33	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥))
17	14, 13, 16	e13 45534	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18		trsbc 45327	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
19	18	biimpd 232	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
20	13, 17, 19	e33 45520	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   Tr 𝑞   )
21		trel 5228	. . . . . . . . . . . 12 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
22	21	expdcom 420	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → (Tr 𝑞 → 𝑧 ∈ 𝑞)))
23	8, 11, 20, 22	e233 45551	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ 𝑞   )
24		elunii 4879	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)
25	24	ex 418	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴))
26	23, 13, 25	e33 45520	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
27	26	in3 45396	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
28	27	gen21 45406	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
29		19.23v 1975	. . . . . . . 8 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ↔ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
30	29	biimpi 219	. . . . . . 7 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
31	28, 30	e2 45418	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
32		pm2.27 43	. . . . . 6 ⊢ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → ((∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
33	6, 31, 32	e22 45458	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
34	33	in2 45392	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
35	34	gen12 45405	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
36		dftr2 5222	. . . 4 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
37	36	biimpri 231	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) → Tr ∪ 𝐴)
38	35, 37	e1a 45414	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∪ 𝐴   )
39	38	in1 45358	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∀wal 1568  ∃wex 1812   ∈ wcel 2146  ∀wral 3081  [wsbc 3746  ∪ cuni 4874  Tr wtr 5220

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737

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 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-v 3459  df-sbc 3747  df-ss 3923  df-uni 4875  df-tr 5221  df-vd1 45357  df-vd2 45365  df-vd3 45377

This theorem is used by: (None)