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 ∪ 𝑥 ∈ 𝐴 𝐵 )