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 )