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

Metamath Proof Explorer

Theorem ixpssmapg

Description: An infinite Cartesian product is a subset of set exponentiation. (Contributed by Jeff Madsen, 19-Jun-2011)

Ref Expression
Assertion ixpssmapg ⊢ ∀ x ∈ A B ∈ V → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A

Proof

Step Hyp Ref Expression
1 n0i ⊢ f ∈ ⨉ x ∈ A B → ¬ ⨉ x ∈ A B = ∅
2 ixpprc ⊢ ¬ A ∈ V → ⨉ x ∈ A B = ∅
3 1 2 nsyl2 ⊢ f ∈ ⨉ x ∈ A B → A ∈ V
4 id ⊢ ∀ x ∈ A B ∈ V → ∀ x ∈ A B ∈ V
5 iunexg ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ V → ⋃ x ∈ A B ∈ V
6 3 4 5 syl2anr ⊢ ∀ x ∈ A B ∈ V ∧ f ∈ ⨉ x ∈ A B → ⋃ x ∈ A B ∈ V
7 ixpssmap2g ⊢ ⋃ x ∈ A B ∈ V → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A
8 6 7 syl ⊢ ∀ x ∈ A B ∈ V ∧ f ∈ ⨉ x ∈ A B → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A
9 simpr ⊢ ∀ x ∈ A B ∈ V ∧ f ∈ ⨉ x ∈ A B → f ∈ ⨉ x ∈ A B
10 8 9 sseldd ⊢ ∀ x ∈ A B ∈ V ∧ f ∈ ⨉ x ∈ A B → f ∈ ⋃ x ∈ A B A
11 10 ex ⊢ ∀ x ∈ A B ∈ V → f ∈ ⨉ x ∈ A B → f ∈ ⋃ x ∈ A B A
12 11 ssrdv ⊢ ∀ x ∈ A B ∈ V → ⨉ x ∈ A B ⊆ ⋃ x ∈ A B A