Metamath Proof Explorer

Theorem f1stres

Description: Mapping of a restriction of the 1st (first member of an ordered pair) function. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion f1stres ⊢ 1 st ↾ A × B : A × B ⟶ A

Proof

Step Hyp Ref Expression
1 vex ⊢ y ∈ V
2 vex ⊢ z ∈ V
3 1 2 op1sta ⊢ ⋃ dom ⁡ y z = y
4 3 eleq1i ⊢ ⋃ dom ⁡ y z ∈ A ↔ y ∈ A
5 4 biranri ⊢ y ∈ A ∧ z ∈ B → ⋃ dom ⁡ y z ∈ A
6 5 rgen2 ⊢ ∀ y ∈ A ∀ z ∈ B ⋃ dom ⁡ y z ∈ A
7 sneq ⊢ x = y z → x = y z
8 7 dmeqd ⊢ x = y z → dom ⁡ x = dom ⁡ y z
9 8 unieqd ⊢ x = y z → ⋃ dom ⁡ x = ⋃ dom ⁡ y z
10 9 eleq1d ⊢ x = y z → ⋃ dom ⁡ x ∈ A ↔ ⋃ dom ⁡ y z ∈ A
11 10 ralxp ⊢ ∀ x ∈ A × B ⋃ dom ⁡ x ∈ A ↔ ∀ y ∈ A ∀ z ∈ B ⋃ dom ⁡ y z ∈ A
12 6 11 mpbir ⊢ ∀ x ∈ A × B ⋃ dom ⁡ x ∈ A
13 df-1st ⊢ 1 st = x ∈ V ⟼ ⋃ dom ⁡ x
14 13 reseq1i ⊢ 1 st ↾ A × B = x ∈ V ⟼ ⋃ dom ⁡ x ↾ A × B
15 ssv ⊢ A × B ⊆ V
16 resmpt ⊢ A × B ⊆ V → x ∈ V ⟼ ⋃ dom ⁡ x ↾ A × B = x ∈ A × B ⟼ ⋃ dom ⁡ x
17 15 16 ax-mp ⊢ x ∈ V ⟼ ⋃ dom ⁡ x ↾ A × B = x ∈ A × B ⟼ ⋃ dom ⁡ x
18 14 17 eqtri ⊢ 1 st ↾ A × B = x ∈ A × B ⟼ ⋃ dom ⁡ x
19 18 fmpt ⊢ ∀ x ∈ A × B ⋃ dom ⁡ x ∈ A ↔ 1 st ↾ A × B : A × B ⟶ A
20 12 19 mpbi ⊢ 1 st ↾ A × B : A × B ⟶ A