Theorem ralssiun

Description: The index set of an indexed union is a subset of the union when each B contains its index. (Contributed by ML, 16-Dec-2020)

	Ref	Expression
Assertion	ralssiun	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfra1	⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵
2		nfcv	⊢ Ⅎ 𝑥 𝐴
3		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
4		simpr	⊢ ( ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
5		rsp	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
6	5	adantl	⊢ ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
7		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
8	7	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) )
9	8	adantr	⊢ ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) )
10	6 9	mpbid	⊢ ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) )
11	10	imp	⊢ ( ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 )
12		rspe	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
13	4 11 12	syl2anc	⊢ ( ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
14		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 )
15	13 14	sylibr	⊢ ( ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } )
16		eleq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ↔ 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ) )
17	16	ad2antrr	⊢ ( ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ↔ 𝑦 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } ) )
18	15 17	mpbird	⊢ ( ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 } )
19		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }
20	18 19	eleqtrrdi	⊢ ( ( ( 𝑥 = 𝑦 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
21	20	expl	⊢ ( 𝑥 = 𝑦 → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
22	21	equcoms	⊢ ( 𝑦 = 𝑥 → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
23	22	vtocleg	⊢ ( 𝑥 ∈ 𝐴 → ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
24	23	anabsi7	⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
25	24	ex	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
26	1 2 3 25	ssrd	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )