Metamath Proof Explorer


Theorem 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 ( ∀ 𝑥𝐴 Tr 𝑥 → Tr 𝐴 )

Proof

Step Hyp Ref Expression
1 simpr ( ( 𝑧𝑦𝑦 𝐴 ) → 𝑦 𝐴 )
2 1 a1i ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → 𝑦 𝐴 ) )
3 eluni ( 𝑦 𝐴 ↔ ∃ 𝑞 ( 𝑦𝑞𝑞𝐴 ) )
4 2 3 syl6ib ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ∃ 𝑞 ( 𝑦𝑞𝑞𝐴 ) ) )
5 simpl ( ( 𝑧𝑦𝑦 𝐴 ) → 𝑧𝑦 )
6 5 a1i ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → 𝑧𝑦 ) )
7 simpl ( ( 𝑦𝑞𝑞𝐴 ) → 𝑦𝑞 )
8 7 2a1i ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ( ( 𝑦𝑞𝑞𝐴 ) → 𝑦𝑞 ) ) )
9 simpr ( ( 𝑦𝑞𝑞𝐴 ) → 𝑞𝐴 )
10 9 2a1i ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ( ( 𝑦𝑞𝑞𝐴 ) → 𝑞𝐴 ) ) )
11 rspsbc ( 𝑞𝐴 → ( ∀ 𝑥𝐴 Tr 𝑥[ 𝑞 / 𝑥 ] Tr 𝑥 ) )
12 11 com12 ( ∀ 𝑥𝐴 Tr 𝑥 → ( 𝑞𝐴[ 𝑞 / 𝑥 ] Tr 𝑥 ) )
13 10 12 syl6d ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ( ( 𝑦𝑞𝑞𝐴 ) → [ 𝑞 / 𝑥 ] Tr 𝑥 ) ) )
14 trsbc ( 𝑞𝐴 → ( [ 𝑞 / 𝑥 ] Tr 𝑥 ↔ Tr 𝑞 ) )
15 14 biimpd ( 𝑞𝐴 → ( [ 𝑞 / 𝑥 ] Tr 𝑥 → Tr 𝑞 ) )
16 10 13 15 ee33 ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ( ( 𝑦𝑞𝑞𝐴 ) → Tr 𝑞 ) ) )
17 trel ( Tr 𝑞 → ( ( 𝑧𝑦𝑦𝑞 ) → 𝑧𝑞 ) )
18 17 expdcom ( 𝑧𝑦 → ( 𝑦𝑞 → ( Tr 𝑞𝑧𝑞 ) ) )
19 6 8 16 18 ee233 ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ( ( 𝑦𝑞𝑞𝐴 ) → 𝑧𝑞 ) ) )
20 elunii ( ( 𝑧𝑞𝑞𝐴 ) → 𝑧 𝐴 )
21 20 ex ( 𝑧𝑞 → ( 𝑞𝐴𝑧 𝐴 ) )
22 19 10 21 ee33 ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ( ( 𝑦𝑞𝑞𝐴 ) → 𝑧 𝐴 ) ) )
23 22 alrimdv ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ∀ 𝑞 ( ( 𝑦𝑞𝑞𝐴 ) → 𝑧 𝐴 ) ) )
24 19.23v ( ∀ 𝑞 ( ( 𝑦𝑞𝑞𝐴 ) → 𝑧 𝐴 ) ↔ ( ∃ 𝑞 ( 𝑦𝑞𝑞𝐴 ) → 𝑧 𝐴 ) )
25 23 24 syl6ib ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → ( ∃ 𝑞 ( 𝑦𝑞𝑞𝐴 ) → 𝑧 𝐴 ) ) )
26 4 25 mpdd ( ∀ 𝑥𝐴 Tr 𝑥 → ( ( 𝑧𝑦𝑦 𝐴 ) → 𝑧 𝐴 ) )
27 26 alrimivv ( ∀ 𝑥𝐴 Tr 𝑥 → ∀ 𝑧𝑦 ( ( 𝑧𝑦𝑦 𝐴 ) → 𝑧 𝐴 ) )
28 dftr2 ( Tr 𝐴 ↔ ∀ 𝑧𝑦 ( ( 𝑧𝑦𝑦 𝐴 ) → 𝑧 𝐴 ) )
29 27 28 sylibr ( ∀ 𝑥𝐴 Tr 𝑥 → Tr 𝐴 )