Theorem truniALT 38751

Description: The union of a class of transitive sets is transitive. Alternate proof of truni 4767. truniALT 38751 is truniALTVD 39114 without virtual deductions and was automatically derived from truniALTVD 39114 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	|- ( A. x e. A Tr x -> Tr U. A )

Distinct variable group:   x, A

Proof of Theorem truniALT

Dummy variables q y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 477	. . . . . 6 |- ( ( z e. y /\ y e. U. A ) -> y e. U. A )
2	1	a1i 11	. . . . 5 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> y e. U. A ) )
3		eluni 4439	. . . . 5 |- ( y e. U. A <-> E. q ( y e. q /\ q e. A ) )
4	2, 3	syl6ib 241	. . . 4 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> E. q ( y e. q /\ q e. A ) ) )
5		simpl 473	. . . . . . . . 9 |- ( ( z e. y /\ y e. U. A ) -> z e. y )
6	5	a1i 11	. . . . . . . 8 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> z e. y ) )
7		simpl 473	. . . . . . . . 9 |- ( ( y e. q /\ q e. A ) -> y e. q )
8	7	2a1i 12	. . . . . . . 8 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> y e. q ) ) )
9		simpr 477	. . . . . . . . . 10 |- ( ( y e. q /\ q e. A ) -> q e. A )
10	9	2a1i 12	. . . . . . . . 9 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> q e. A ) ) )
11		rspsbc 3518	. . . . . . . . . . 11 |- ( q e. A -> ( A. x e. A Tr x -> [. q / x ]. Tr x ) )
12	11	com12 32	. . . . . . . . . 10 |- ( A. x e. A Tr x -> ( q e. A -> [. q / x ]. Tr x ) )
13	10, 12	syl6d 75	. . . . . . . . 9 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> [. q / x ]. Tr x ) ) )
14		trsbc 38750	. . . . . . . . . 10 |- ( q e. A -> ( [. q / x ]. Tr x <-> Tr q ) )
15	14	biimpd 219	. . . . . . . . 9 |- ( q e. A -> ( [. q / x ]. Tr x -> Tr q ) )
16	10, 13, 15	ee33 38727	. . . . . . . 8 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> Tr q ) ) )
17		trel 4759	. . . . . . . . 9 |- ( Tr q -> ( ( z e. y /\ y e. q ) -> z e. q ) )
18	17	expdcom 455	. . . . . . . 8 |- ( z e. y -> ( y e. q -> ( Tr q -> z e. q ) ) )
19	6, 8, 16, 18	ee233 38725	. . . . . . 7 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> z e. q ) ) )
20		elunii 4441	. . . . . . . 8 |- ( ( z e. q /\ q e. A ) -> z e. U. A )
21	20	ex 450	. . . . . . 7 |- ( z e. q -> ( q e. A -> z e. U. A ) )
22	19, 10, 21	ee33 38727	. . . . . 6 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> ( ( y e. q /\ q e. A ) -> z e. U. A ) ) )
23	22	alrimdv 1857	. . . . 5 |- ( 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 ) ) )
24		19.23v 1902	. . . . 5 |- ( A. q ( ( y e. q /\ q e. A ) -> z e. U. A ) <-> ( E. q ( y e. q /\ q e. A ) -> z e. U. A ) )
25	23, 24	syl6ib 241	. . . 4 |- ( 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 ) ) )
26	4, 25	mpdd 43	. . 3 |- ( A. x e. A Tr x -> ( ( z e. y /\ y e. U. A ) -> z e. U. A ) )
27	26	alrimivv 1856	. 2 |- ( A. x e. A Tr x -> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) )
28		dftr2 4754	. 2 |- ( Tr U. A <-> A. z A. y ( ( z e. y /\ y e. U. A ) -> z e. U. A ) )
29	27, 28	sylibr 224	1 |- ( A. x e. A Tr x -> Tr U. A )

Syntax hints:   -> wi 4   /\ wa 384   A.wal 1481   E.wex 1704   e. wcel 1990   A.wral 2912   [.wsbc 3435   U.cuni 4436   Tr wtr 4752

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-sbc 3436  df-in 3581  df-ss 3588  df-uni 4437  df-tr 4753

This theorem is referenced by: (None)