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

Metamath Proof Explorer

Theorem genpdm

Description: Domain of general operation on positive reals. (Contributed by NM, 18-Nov-1995) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 ⊢ F = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
Assertion genpdm ⊢ dom ⁡ F = 𝑷 × 𝑷

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ F = w ∈ 𝑷 , v ∈ 𝑷 ⟼ x | ∃ y ∈ w ∃ z ∈ v x = y G z
2 genp.2 ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → y G z ∈ 𝑸
3 elprnq ⊢ w ∈ 𝑷 ∧ y ∈ w → y ∈ 𝑸
4 elprnq ⊢ v ∈ 𝑷 ∧ z ∈ v → z ∈ 𝑸
5 eleq1 ⊢ x = y G z → x ∈ 𝑸 ↔ y G z ∈ 𝑸
6 2 5 syl5ibrcom ⊢ y ∈ 𝑸 ∧ z ∈ 𝑸 → x = y G z → x ∈ 𝑸
7 3 4 6 syl2an ⊢ w ∈ 𝑷 ∧ y ∈ w ∧ v ∈ 𝑷 ∧ z ∈ v → x = y G z → x ∈ 𝑸
8 7 an4s ⊢ w ∈ 𝑷 ∧ v ∈ 𝑷 ∧ y ∈ w ∧ z ∈ v → x = y G z → x ∈ 𝑸
9 8 rexlimdvva ⊢ w ∈ 𝑷 ∧ v ∈ 𝑷 → ∃ y ∈ w ∃ z ∈ v x = y G z → x ∈ 𝑸
10 9 abssdv ⊢ w ∈ 𝑷 ∧ v ∈ 𝑷 → x | ∃ y ∈ w ∃ z ∈ v x = y G z ⊆ 𝑸
11 nqex ⊢ 𝑸 ∈ V
12 ssexg ⊢ x | ∃ y ∈ w ∃ z ∈ v x = y G z ⊆ 𝑸 ∧ 𝑸 ∈ V → x | ∃ y ∈ w ∃ z ∈ v x = y G z ∈ V
13 10 11 12 sylancl ⊢ w ∈ 𝑷 ∧ v ∈ 𝑷 → x | ∃ y ∈ w ∃ z ∈ v x = y G z ∈ V
14 13 rgen2 ⊢ ∀ w ∈ 𝑷 ∀ v ∈ 𝑷 x | ∃ y ∈ w ∃ z ∈ v x = y G z ∈ V
15 1 fnmpo ⊢ ∀ w ∈ 𝑷 ∀ v ∈ 𝑷 x | ∃ y ∈ w ∃ z ∈ v x = y G z ∈ V → F Fn 𝑷 × 𝑷
16 fndm ⊢ F Fn 𝑷 × 𝑷 → dom ⁡ F = 𝑷 × 𝑷
17 14 15 16 mp2b ⊢ dom ⁡ F = 𝑷 × 𝑷