truniALTVD

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

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

Proof

Step	Hyp	Ref	Expression
1		idn2	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to (z \in y \land y \in ⋃ A))$
2		simpr	$⊢ (z \in y \land y \in ⋃ A) \to y \in ⋃ A$
3	1 2	e2	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to y \in ⋃ A)$
4		eluni	$⊢ y \in ⋃ A \leftrightarrow \exists q (y \in q \land q \in A)$
5	4	biimpi	$⊢ y \in ⋃ A \to \exists q (y \in q \land q \in A)$
6	3 5	e2	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to \exists q (y \in q \land q \in A))$
7		simpl	$⊢ (z \in y \land y \in ⋃ A) \to z \in y$
8	1 7	e2	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to z \in y)$
9		idn3	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A), (y \in q \land q \in A) \to (y \in q \land q \in A))$
10		simpl	$⊢ (y \in q \land q \in A) \to y \in q$
11	9 10	e3	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A), (y \in q \land q \in A) \to y \in q)$
12		simpr	$⊢ (y \in q \land q \in A) \to q \in A$
13	9 12	e3	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A), (y \in q \land q \in A) \to q \in A)$
14		idn1	$⊢ (\forall x \in A Tr x \to \forall x \in A Tr x)$
15		rspsbc	$⊢ q \in A \to (\forall x \in A Tr x \to \underset{˙}{[} q / x \underset{˙}{]} Tr x)$
16	15	com12	$⊢ \forall x \in A Tr x \to (q \in A \to \underset{˙}{[} q / x \underset{˙}{]} Tr x)$
17	14 13 16	e13	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A), (y \in q \land q \in A) \to \underset{˙}{[} q / x \underset{˙}{]} Tr x)$
18		trsbc	$⊢ q \in A \to (\underset{˙}{[} q / x \underset{˙}{]} Tr x \leftrightarrow Tr q)$
19	18	biimpd	$⊢ q \in A \to (\underset{˙}{[} q / x \underset{˙}{]} Tr x \to Tr q)$
20	13 17 19	e33	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A), (y \in q \land q \in A) \to Tr q)$
21		trel	$⊢ Tr q \to ((z \in y \land y \in q) \to z \in q)$
22	21	expdcom	$⊢ z \in y \to (y \in q \to (Tr q \to z \in q))$
23	8 11 20 22	e233	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A), (y \in q \land q \in A) \to z \in q)$
24		elunii	$⊢ (z \in q \land q \in A) \to z \in ⋃ A$
25	24	ex	$⊢ z \in q \to (q \in A \to z \in ⋃ A)$
26	23 13 25	e33	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A), (y \in q \land q \in A) \to z \in ⋃ A)$
27	26	in3	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to ((y \in q \land q \in A) \to z \in ⋃ A))$
28	27	gen21	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to \forall q ((y \in q \land q \in A) \to z \in ⋃ A))$
29		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)$
30	29	biimpi	$⊢ \forall q ((y \in q \land q \in A) \to z \in ⋃ A) \to (\exists q (y \in q \land q \in A) \to z \in ⋃ A)$
31	28 30	e2	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to (\exists q (y \in q \land q \in A) \to z \in ⋃ A))$
32		pm2.27	$⊢ \exists q (y \in q \land q \in A) \to ((\exists q (y \in q \land q \in A) \to z \in ⋃ A) \to z \in ⋃ A)$
33	6 31 32	e22	$⊢ (\forall x \in A Tr x, (z \in y \land y \in ⋃ A) \to z \in ⋃ A)$
34	33	in2	$⊢ (\forall x \in A Tr x \to ((z \in y \land y \in ⋃ A) \to z \in ⋃ A))$
35	34	gen12	$⊢ (\forall x \in A Tr x \to \forall z \forall y ((z \in y \land y \in ⋃ A) \to z \in ⋃ A))$
36		dftr2	$⊢ Tr ⋃ A \leftrightarrow \forall z \forall y ((z \in y \land y \in ⋃ A) \to z \in ⋃ A)$
37	36	biimpri	$⊢ \forall z \forall y ((z \in y \land y \in ⋃ A) \to z \in ⋃ A) \to Tr ⋃ A$
38	35 37	e1a	$⊢ (\forall x \in A Tr x \to Tr ⋃ A)$
39	38	in1	$⊢ \forall x \in A Tr x \to Tr ⋃ A$

1::	\|- (. A. x e. A Tr x ->. A. x e. A Tr x ).
2::	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( z e. y /\ y e. U. A ) ).
3:2:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. z e. y ).
4:2:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. y e. U. A ).
5:4:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. E. q ( y e. q /\ q e. A ) ).
6::	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) , ( y e. q /\ q e. A ) ->. ( y e. q /\ q e. A ) ).
7:6:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) , ( y e. q /\ q e. A ) ->. y e. q ).
8:6:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) , ( y e. q /\ q e. A ) ->. q e. A ).
9:1,8:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) , ( y e. q /\ q e. A ) ->. [ q / x ] Tr x ).
10:8,9:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) , ( y e. q /\ q e. A ) ->. Tr q ).
11:3,7,10:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) , ( y e. q /\ q e. A ) ->. z e. q ).
12:11,8:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) , ( y e. q /\ q e. A ) ->. z e. U. A ).
13:12:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( ( y e. q /\ q e. A ) -> z e. U. A ) ).
14:13:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. A. q ( ( y e. q /\ q e. A ) -> z e. U. A ) ).
15:14:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) ).
16:5,15:	\|- (. A. x e. A Tr x ,. ( z e. y /\ y e. U. A ) ->. z e. U. A ).
17:16:	\|- (. A. x e. A Tr x ->. ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ).
18:17:	\|- (. A. x e. A Tr x ->. A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) ).
19:18:	\|- (. A. x e. A Tr x ->. Tr U. A ).
qed:19:	\|- ( A. x e. A Tr x -> Tr U. A )

Metamath Proof Explorer

Theorem truniALTVD

Proof