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 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
Assertion genpdm dom 𝐹 = ( P × P )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 elprnq ⊢ ( ( 𝑤 ∈ P ∧ 𝑦 ∈ 𝑤 ) → 𝑦 ∈ Q )
4 elprnq ⊢ ( ( 𝑣 ∈ P ∧ 𝑧 ∈ 𝑣 ) → 𝑧 ∈ Q )
5 eleq1 ⊢ ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → ( 𝑥 ∈ Q ↔ ( 𝑦 𝐺 𝑧 ) ∈ Q ) )
6 2 5 syl5ibrcom ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
7 3 4 6 syl2an ⊢ ( ( ( 𝑤 ∈ P ∧ 𝑦 ∈ 𝑤 ) ∧ ( 𝑣 ∈ P ∧ 𝑧 ∈ 𝑣 ) ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
8 7 an4s ⊢ ( ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) ∧ ( 𝑦 ∈ 𝑤 ∧ 𝑧 ∈ 𝑣 ) ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
9 8 rexlimdvva ⊢ ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) → ( ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
10 9 abssdv ⊢ ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } ⊆ Q )
11 nqex ⊢ Q ∈ V
12 ssexg ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } ⊆ Q ∧ Q ∈ V ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V )
13 10 11 12 sylancl ⊢ ( ( 𝑤 ∈ P ∧ 𝑣 ∈ P ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V )
14 13 rgen2 ⊢ ∀ 𝑤 ∈ P ∀ 𝑣 ∈ P { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V
15 1 fnmpo ⊢ ( ∀ 𝑤 ∈ P ∀ 𝑣 ∈ P { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V → 𝐹 Fn ( P × P ) )
16 fndm ⊢ ( 𝐹 Fn ( P × P ) → dom 𝐹 = ( P × P ) )
17 14 15 16 mp2b ⊢ dom 𝐹 = ( P × P )