This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem triun

Description: An indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion triun ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
2 r19.29 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ( Tr 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
3 nfcv ⊢ Ⅎ 𝑥 𝑦
4 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
5 3 4 nfss ⊢ Ⅎ 𝑥 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵
6 trss ⊢ ( Tr 𝐵 → ( 𝑦 ∈ 𝐵 → 𝑦 ⊆ 𝐵 ) )
7 6 imp ⊢ ( ( Tr 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ⊆ 𝐵 )
8 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
9 sstr2 ⊢ ( 𝑦 ⊆ 𝐵 → ( 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
10 7 8 9 syl2imc ⊢ ( 𝑥 ∈ 𝐴 → ( ( Tr 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
11 5 10 rexlimi ⊢ ( ∃ 𝑥 ∈ 𝐴 ( Tr 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
12 2 11 syl ⊢ ( ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 ) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
13 1 12 sylan2b ⊢ ( ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
14 13 ralrimiva ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 → ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
15 dftr3 ⊢ ( Tr ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝑦 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
16 14 15 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 Tr 𝐵 → Tr ∪ 𝑥 ∈ 𝐴 𝐵 )