truniALT

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

		Ref	Expression
	Assertion	truniALT	$⊢ \forall x \in A Tr x \to Tr ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (z \in y \land y \in ⋃ A) \to y \in ⋃ A$
2	1	a1i	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to y \in ⋃ A)$
3		eluni	$⊢ y \in ⋃ A \leftrightarrow \exists q (y \in q \land q \in A)$
4	2 3	syl6ib	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to \exists q (y \in q \land q \in A))$
5		simpl	$⊢ (z \in y \land y \in ⋃ A) \to z \in y$
6	5	a1i	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to z \in y)$
7		simpl	$⊢ (y \in q \land q \in A) \to y \in q$
8	7	2a1i	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to ((y \in q \land q \in A) \to y \in q))$
9		simpr	$⊢ (y \in q \land q \in A) \to q \in A$
10	9	2a1i	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to ((y \in q \land q \in A) \to q \in A))$
11		rspsbc	$⊢ q \in A \to (\forall x \in A Tr x \to \underset{˙}{[} q / x \underset{˙}{]} Tr x)$
12	11	com12	$⊢ \forall x \in A Tr x \to (q \in A \to \underset{˙}{[} q / x \underset{˙}{]} Tr x)$
13	10 12	syl6d	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to ((y \in q \land q \in A) \to \underset{˙}{[} q / x \underset{˙}{]} Tr x))$
14		trsbc	$⊢ q \in A \to (\underset{˙}{[} q / x \underset{˙}{]} Tr x \leftrightarrow Tr q)$
15	14	biimpd	$⊢ q \in A \to (\underset{˙}{[} q / x \underset{˙}{]} Tr x \to Tr q)$
16	10 13 15	ee33	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to ((y \in q \land q \in A) \to Tr q))$
17		trel	$⊢ Tr q \to ((z \in y \land y \in q) \to z \in q)$
18	17	expdcom	$⊢ z \in y \to (y \in q \to (Tr q \to z \in q))$
19	6 8 16 18	ee233	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to ((y \in q \land q \in A) \to z \in q))$
20		elunii	$⊢ (z \in q \land q \in A) \to z \in ⋃ A$
21	20	ex	$⊢ z \in q \to (q \in A \to z \in ⋃ A)$
22	19 10 21	ee33	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to ((y \in q \land q \in A) \to z \in ⋃ A))$
23	22	alrimdv	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to \forall q ((y \in q \land q \in A) \to z \in ⋃ A))$
24		19.23v	$⊢ \forall q ((y \in q \land q \in A) \to z \in ⋃ A) \leftrightarrow (\exists q (y \in q \land q \in A) \to z \in ⋃ A)$
25	23 24	syl6ib	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to (\exists q (y \in q \land q \in A) \to z \in ⋃ A))$
26	4 25	mpdd	$⊢ \forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to z \in ⋃ A)$
27	26	alrimivv	$⊢ \forall x \in A Tr x \to \forall z \forall y ((z \in y \land y \in ⋃ A) \to z \in ⋃ A)$
28		dftr2	$⊢ Tr ⋃ A \leftrightarrow \forall z \forall y ((z \in y \land y \in ⋃ A) \to z \in ⋃ A)$
29	27 28	sylibr	$⊢ \forall x \in A Tr x \to Tr ⋃ A$

Metamath Proof Explorer

Theorem truniALT

Proof