Theorem truniALTVD 42468

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

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 42203	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   )
2		simpr 485	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴)
3	1, 2	e2 42221	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑦 ∈ ∪ 𝐴   )
4		eluni 4844	. . . . . . . 8 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
5	4	biimpi 215	. . . . . . 7 ⊢ (𝑦 ∈ ∪ 𝐴 → ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
6	3, 5	e2 42221	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
7		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦)
8	1, 7	e2 42221	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ 𝑦   )
9		idn3 42205	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   )
10		simpl 483	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞)
11	9, 10	e3 42327	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑦 ∈ 𝑞   )
12		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)
13	9, 12	e3 42327	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑞 ∈ 𝐴   )
14		idn1 42164	. . . . . . . . . . . . 13 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑥 ∈ 𝐴 Tr 𝑥   )
15		rspsbc 3813	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
16	15	com12 32	. . . . . . . . . . . . 13 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥))
17	14, 13, 16	e13 42338	. . . . . . . . . . . 12 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   [𝑞 / 𝑥]Tr 𝑥   )
18		trsbc 42130	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
19	18	biimpd 228	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
20	13, 17, 19	e33 42324	. . . . . . . . . . 11 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   Tr 𝑞   )
21		trel 5200	. . . . . . . . . . . 12 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
22	21	expdcom 415	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → (Tr 𝑞 → 𝑧 ∈ 𝑞)))
23	8, 11, 20, 22	e233 42355	. . . . . . . . . 10 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ 𝑞   )
24		elunii 4846	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)
25	24	ex 413	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴))
26	23, 13, 25	e33 42324	. . . . . . . . 9 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ,   (𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
27	26	in3 42199	. . . . . . . 8 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
28	27	gen21 42209	. . . . . . 7 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   ∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
29		19.23v 1945	. . . . . . . 8 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ↔ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
30	29	biimpi 215	. . . . . . 7 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
31	28, 30	e2 42221	. . . . . 6 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
32		pm2.27 42	. . . . . 6 ⊢ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → ((∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
33	6, 31, 32	e22 42261	. . . . 5 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴)   ▶   𝑧 ∈ ∪ 𝐴   )
34	33	in2 42195	. . . 4 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
35	34	gen12 42208	. . 3 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴)   )
36		dftr2 5195	. . . 4 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
37	36	biimpri 227	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴) → Tr ∪ 𝐴)
38	35, 37	e1a 42217	. 2 ⊢ (   ∀𝑥 ∈ 𝐴 Tr 𝑥   ▶   Tr ∪ 𝐴   )
39	38	in1 42161	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1537  ∃wex 1782   ∈ wcel 2106  ∀wral 3064  [wsbc 3717  ∪ cuni 4841  Tr wtr 5193

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-v 3433  df-sbc 3718  df-in 3895  df-ss 3905  df-uni 4842  df-tr 5194  df-vd1 42160  df-vd2 42168  df-vd3 42180

This theorem is referenced by: (None)