Theorem truniALT 43384

Description: The union of a class of transitive sets is transitive. Alternate proof of truni 5281. truniALT 43384 is truniALTVD 43721 without virtual deductions and was automatically derived from truniALTVD 43721 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

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

Distinct variable group:   𝑥,𝐴

Proof of Theorem truniALT

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

Step	Hyp	Ref	Expression
1		simpr 485	. . . . . 6 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴)
2	1	a1i 11	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑦 ∈ ∪ 𝐴))
3		eluni 4911	. . . . 5 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴))
4	2, 3	imbitrdi 250	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴)))
5		simpl 483	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦)
6	5	a1i 11	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ 𝑦))
7		simpl 483	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞)
8	7	2a1i 12	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑦 ∈ 𝑞)))
9		simpr 485	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)
10	9	2a1i 12	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑞 ∈ 𝐴)))
11		rspsbc 3873	. . . . . . . . . . 11 ⊢ (𝑞 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Tr 𝑥 → [𝑞 / 𝑥]Tr 𝑥))
12	11	com12 32	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → (𝑞 ∈ 𝐴 → [𝑞 / 𝑥]Tr 𝑥))
13	10, 12	syl6d 75	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → [𝑞 / 𝑥]Tr 𝑥)))
14		trsbc 43383	. . . . . . . . . 10 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 ↔ Tr 𝑞))
15	14	biimpd 228	. . . . . . . . 9 ⊢ (𝑞 ∈ 𝐴 → ([𝑞 / 𝑥]Tr 𝑥 → Tr 𝑞))
16	10, 13, 15	ee33 43364	. . . . . . . 8 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → Tr 𝑞)))
17		trel 5274	. . . . . . . . 9 ⊢ (Tr 𝑞 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑞) → 𝑧 ∈ 𝑞))
18	17	expdcom 415	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑦 → (𝑦 ∈ 𝑞 → (Tr 𝑞 → 𝑧 ∈ 𝑞)))
19	6, 8, 16, 18	ee233 43362	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ 𝑞)))
20		elunii 4913	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)
21	20	ex 413	. . . . . . 7 ⊢ (𝑧 ∈ 𝑞 → (𝑞 ∈ 𝐴 → 𝑧 ∈ ∪ 𝐴))
22	19, 10, 21	ee33 43364	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)))
23	22	alrimdv 1932	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → ∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)))
24		19.23v 1945	. . . . 5 ⊢ (∀𝑞((𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴) ↔ (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴))
25	23, 24	imbitrdi 250	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → (∃𝑞(𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴) → 𝑧 ∈ ∪ 𝐴)))
26	4, 25	mpdd 43	. . 3 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
27	26	alrimivv 1931	. 2 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
28		dftr2 5267	. 2 ⊢ (Tr ∪ 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴) → 𝑧 ∈ ∪ 𝐴))
29	27, 28	sylibr 233	1 ⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1539  ∃wex 1781   ∈ wcel 2106  ∀wral 3061  [wsbc 3777  ∪ cuni 4908  Tr wtr 5265

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-v 3476  df-sbc 3778  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266

This theorem is referenced by: (None)