Theorem marypha2lem1

Description: Lemma for marypha2 . Properties of the used relation. (Contributed by Stefan O'Rear, 20-Feb-2015)

	Ref	Expression
Hypothesis	marypha2lem.t	⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
Assertion	marypha2lem1	⊢ 𝑇 ⊆ ( 𝐴 × ∪ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		marypha2lem.t	⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) )
2		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝐴 × ∪ ran 𝐹 ) ↔ ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝐴 × ∪ ran 𝐹 ) )
3		snssi	⊢ ( 𝑥 ∈ 𝐴 → { 𝑥 } ⊆ 𝐴 )
4		fvssunirn	⊢ ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ran 𝐹
5		xpss12	⊢ ( ( { 𝑥 } ⊆ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ⊆ ∪ ran 𝐹 ) → ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝐴 × ∪ ran 𝐹 ) )
6	3 4 5	sylancl	⊢ ( 𝑥 ∈ 𝐴 → ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝐴 × ∪ ran 𝐹 ) )
7	2 6	mprgbir	⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × ( 𝐹 ‘ 𝑥 ) ) ⊆ ( 𝐴 × ∪ ran 𝐹 )
8	1 7	eqsstri	⊢ 𝑇 ⊆ ( 𝐴 × ∪ ran 𝐹 )