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

Metamath Proof Explorer

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 𝐹 )