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 imbitrdi ⊢ ( ∀ 𝑥 ∈ 𝐴 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 imbitrdi ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴 ) → ( ∃ 𝑞 ( 𝑦 ∈ 𝑞 ∧ 𝑞 ∈ 𝐴 ) → 𝑧 ∈ ∪ 𝐴 ) ) )
26 4 25 mpdd ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴 ) → 𝑧 ∈ ∪ 𝐴 ) )
27 26 alrimivv ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴 ) → 𝑧 ∈ ∪ 𝐴 ) )
28 dftr2 ⊢ ( Tr ∪ 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ∪ 𝐴 ) → 𝑧 ∈ ∪ 𝐴 ) )
29 27 28 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴 )