genipv - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > genipv		GIF version

Theorem genipv 6492

Description: Value of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingon, 3-Oct-2019.)

**Hypotheses**
Ref	Expression
genp.1	⊢ 𝐹 = (w ∈ P, v ∈ P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘w) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘w) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))}⟩)
genp.2	⊢ ((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q)

**Assertion**
Ref	Expression
genipv	⊢ ((A ∈ P ∧ B ∈ P) → (A𝐹B) = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^st ‘A)∃𝑠 ∈ (1^st ‘B)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^nd ‘A)∃𝑠 ∈ (2^nd ‘B)𝑞 = (𝑟𝐺𝑠)}⟩)

Distinct variable groups: x,y,z,𝑞,𝑟,𝑠,A x,B,y,z,𝑞,𝑟,𝑠 x,w,v,𝐺,y,z,𝑞,𝑟,𝑠 Allowed substitution hints: A(w,v) B(w,v) 𝐹(x,y,z,w,v,𝑠,𝑟,𝑞)

Proof of Theorem genipv Dummy variables f g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 5462	. . . 4 ⊢ (f = A → (f𝐹g) = (A𝐹g))
2		fveq2 5121	. . . . . . 7 ⊢ (f = A → (1^st ‘f) = (1^st ‘A))
3	2	rexeqdv 2506	. . . . . 6 ⊢ (f = A → (∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z) ↔ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z)))
4	3	rabbidv 2543	. . . . 5 ⊢ (f = A → {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z)})
5		fveq2 5121	. . . . . . 7 ⊢ (f = A → (2^nd ‘f) = (2^nd ‘A))
6	5	rexeqdv 2506	. . . . . 6 ⊢ (f = A → (∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z) ↔ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z)))
7	6	rabbidv 2543	. . . . 5 ⊢ (f = A → {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z)})
8	4, 7	opeq12d 3548	. . . 4 ⊢ (f = A → ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩ = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩)
9	1, 8	eqeq12d 2051	. . 3 ⊢ (f = A → ((f𝐹g) = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩ ↔ (A𝐹g) = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩))
10		oveq2 5463	. . . 4 ⊢ (g = B → (A𝐹g) = (A𝐹B))
11		fveq2 5121	. . . . . . . 8 ⊢ (g = B → (1^st ‘g) = (1^st ‘B))
12	11	rexeqdv 2506	. . . . . . 7 ⊢ (g = B → (∃z ∈ (1^st ‘g)x = (y𝐺z) ↔ ∃z ∈ (1^st ‘B)x = (y𝐺z)))
13	12	rexbidv 2321	. . . . . 6 ⊢ (g = B → (∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z) ↔ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)))
14	13	rabbidv 2543	. . . . 5 ⊢ (g = B → {x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)})
15		fveq2 5121	. . . . . . . 8 ⊢ (g = B → (2^nd ‘g) = (2^nd ‘B))
16	15	rexeqdv 2506	. . . . . . 7 ⊢ (g = B → (∃z ∈ (2^nd ‘g)x = (y𝐺z) ↔ ∃z ∈ (2^nd ‘B)x = (y𝐺z)))
17	16	rexbidv 2321	. . . . . 6 ⊢ (g = B → (∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z) ↔ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z)))
18	17	rabbidv 2543	. . . . 5 ⊢ (g = B → {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z)})
19	14, 18	opeq12d 3548	. . . 4 ⊢ (g = B → ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩ = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z)}⟩)
20	10, 19	eqeq12d 2051	. . 3 ⊢ (g = B → ((A𝐹g) = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩ ↔ (A𝐹B) = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z)}⟩))
21		nqex 6347	. . . . . . 7 ⊢ Q ∈ V
22	21	a1i 9	. . . . . 6 ⊢ ((f ∈ P ∧ g ∈ P) → Q ∈ V)
23		rabssab 3021	. . . . . . 7 ⊢ {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ⊆ {x ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}
24		prop 6458	. . . . . . . . . . . 12 ⊢ (f ∈ P → ⟨(1^st ‘f), (2^nd ‘f)⟩ ∈ P)
25		elprnql 6464	. . . . . . . . . . . 12 ⊢ ((⟨(1^st ‘f), (2^nd ‘f)⟩ ∈ P ∧ y ∈ (1^st ‘f)) → y ∈ Q)
26	24, 25	sylan 267	. . . . . . . . . . 11 ⊢ ((f ∈ P ∧ y ∈ (1^st ‘f)) → y ∈ Q)
27		prop 6458	. . . . . . . . . . . 12 ⊢ (g ∈ P → ⟨(1^st ‘g), (2^nd ‘g)⟩ ∈ P)
28		elprnql 6464	. . . . . . . . . . . 12 ⊢ ((⟨(1^st ‘g), (2^nd ‘g)⟩ ∈ P ∧ z ∈ (1^st ‘g)) → z ∈ Q)
29	27, 28	sylan 267	. . . . . . . . . . 11 ⊢ ((g ∈ P ∧ z ∈ (1^st ‘g)) → z ∈ Q)
30		genp.2	. . . . . . . . . . . 12 ⊢ ((y ∈ Q ∧ z ∈ Q) → (y𝐺z) ∈ Q)
31		eleq1 2097	. . . . . . . . . . . 12 ⊢ (x = (y𝐺z) → (x ∈ Q ↔ (y𝐺z) ∈ Q))
32	30, 31	syl5ibrcom 146	. . . . . . . . . . 11 ⊢ ((y ∈ Q ∧ z ∈ Q) → (x = (y𝐺z) → x ∈ Q))
33	26, 29, 32	syl2an 273	. . . . . . . . . 10 ⊢ (((f ∈ P ∧ y ∈ (1^st ‘f)) ∧ (g ∈ P ∧ z ∈ (1^st ‘g))) → (x = (y𝐺z) → x ∈ Q))
34	33	an4s 522	. . . . . . . . 9 ⊢ (((f ∈ P ∧ g ∈ P) ∧ (y ∈ (1^st ‘f) ∧ z ∈ (1^st ‘g))) → (x = (y𝐺z) → x ∈ Q))
35	34	rexlimdvva 2434	. . . . . . . 8 ⊢ ((f ∈ P ∧ g ∈ P) → (∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z) → x ∈ Q))
36	35	abssdv 3008	. . . . . . 7 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ⊆ Q)
37	23, 36	syl5ss 2950	. . . . . 6 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ⊆ Q)
38	22, 37	ssexd 3888	. . . . 5 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ∈ V)
39		rabssab 3021	. . . . . . 7 ⊢ {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ⊆ {x ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}
40		elprnqu 6465	. . . . . . . . . . . 12 ⊢ ((⟨(1^st ‘f), (2^nd ‘f)⟩ ∈ P ∧ y ∈ (2^nd ‘f)) → y ∈ Q)
41	24, 40	sylan 267	. . . . . . . . . . 11 ⊢ ((f ∈ P ∧ y ∈ (2^nd ‘f)) → y ∈ Q)
42		elprnqu 6465	. . . . . . . . . . . 12 ⊢ ((⟨(1^st ‘g), (2^nd ‘g)⟩ ∈ P ∧ z ∈ (2^nd ‘g)) → z ∈ Q)
43	27, 42	sylan 267	. . . . . . . . . . 11 ⊢ ((g ∈ P ∧ z ∈ (2^nd ‘g)) → z ∈ Q)
44	41, 43, 32	syl2an 273	. . . . . . . . . 10 ⊢ (((f ∈ P ∧ y ∈ (2^nd ‘f)) ∧ (g ∈ P ∧ z ∈ (2^nd ‘g))) → (x = (y𝐺z) → x ∈ Q))
45	44	an4s 522	. . . . . . . . 9 ⊢ (((f ∈ P ∧ g ∈ P) ∧ (y ∈ (2^nd ‘f) ∧ z ∈ (2^nd ‘g))) → (x = (y𝐺z) → x ∈ Q))
46	45	rexlimdvva 2434	. . . . . . . 8 ⊢ ((f ∈ P ∧ g ∈ P) → (∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z) → x ∈ Q))
47	46	abssdv 3008	. . . . . . 7 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ⊆ Q)
48	39, 47	syl5ss 2950	. . . . . 6 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ⊆ Q)
49	22, 48	ssexd 3888	. . . . 5 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ∈ V)
50		opelxp 4317	. . . . 5 ⊢ (⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩ ∈ (V × V) ↔ ({x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ∈ V ∧ {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ∈ V))
51	38, 49, 50	sylanbrc 394	. . . 4 ⊢ ((f ∈ P ∧ g ∈ P) → ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩ ∈ (V × V))
52		fveq2 5121	. . . . . . . 8 ⊢ (w = f → (1^st ‘w) = (1^st ‘f))
53	52	rexeqdv 2506	. . . . . . 7 ⊢ (w = f → (∃y ∈ (1^st ‘w)∃z ∈ (1^st ‘v)x = (y𝐺z) ↔ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘v)x = (y𝐺z)))
54	53	rabbidv 2543	. . . . . 6 ⊢ (w = f → {x ∈ Q ∣ ∃y ∈ (1^st ‘w)∃z ∈ (1^st ‘v)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘v)x = (y𝐺z)})
55		fveq2 5121	. . . . . . . 8 ⊢ (w = f → (2^nd ‘w) = (2^nd ‘f))
56	55	rexeqdv 2506	. . . . . . 7 ⊢ (w = f → (∃y ∈ (2^nd ‘w)∃z ∈ (2^nd ‘v)x = (y𝐺z) ↔ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘v)x = (y𝐺z)))
57	56	rabbidv 2543	. . . . . 6 ⊢ (w = f → {x ∈ Q ∣ ∃y ∈ (2^nd ‘w)∃z ∈ (2^nd ‘v)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘v)x = (y𝐺z)})
58	54, 57	opeq12d 3548	. . . . 5 ⊢ (w = f → ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘w)∃z ∈ (1^st ‘v)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘w)∃z ∈ (2^nd ‘v)x = (y𝐺z)}⟩ = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘v)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘v)x = (y𝐺z)}⟩)
59		fveq2 5121	. . . . . . . . 9 ⊢ (v = g → (1^st ‘v) = (1^st ‘g))
60	59	rexeqdv 2506	. . . . . . . 8 ⊢ (v = g → (∃z ∈ (1^st ‘v)x = (y𝐺z) ↔ ∃z ∈ (1^st ‘g)x = (y𝐺z)))
61	60	rexbidv 2321	. . . . . . 7 ⊢ (v = g → (∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘v)x = (y𝐺z) ↔ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)))
62	61	rabbidv 2543	. . . . . 6 ⊢ (v = g → {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘v)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)})
63		fveq2 5121	. . . . . . . . 9 ⊢ (v = g → (2^nd ‘v) = (2^nd ‘g))
64	63	rexeqdv 2506	. . . . . . . 8 ⊢ (v = g → (∃z ∈ (2^nd ‘v)x = (y𝐺z) ↔ ∃z ∈ (2^nd ‘g)x = (y𝐺z)))
65	64	rexbidv 2321	. . . . . . 7 ⊢ (v = g → (∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘v)x = (y𝐺z) ↔ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)))
66	65	rabbidv 2543	. . . . . 6 ⊢ (v = g → {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘v)x = (y𝐺z)} = {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)})
67	62, 66	opeq12d 3548	. . . . 5 ⊢ (v = g → ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘v)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘v)x = (y𝐺z)}⟩ = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩)
68		genp.1	. . . . . 6 ⊢ 𝐹 = (w ∈ P, v ∈ P ↦ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘w) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘w) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))}⟩)
69	68	genpdf 6491	. . . . 5 ⊢ 𝐹 = (w ∈ P, v ∈ P ↦ ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘w)∃z ∈ (1^st ‘v)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘w)∃z ∈ (2^nd ‘v)x = (y𝐺z)}⟩)
70	58, 67, 69	ovmpt2g 5577	. . . 4 ⊢ ((f ∈ P ∧ g ∈ P ∧ ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩ ∈ (V × V)) → (f𝐹g) = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩)
71	51, 70	mpd3an3 1232	. . 3 ⊢ ((f ∈ P ∧ g ∈ P) → (f𝐹g) = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)}⟩)
72	9, 20, 71	vtocl2ga 2615	. 2 ⊢ ((A ∈ P ∧ B ∈ P) → (A𝐹B) = ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z)}⟩)
73		eqeq1 2043	. . . . . 6 ⊢ (x = 𝑞 → (x = (y𝐺z) ↔ 𝑞 = (y𝐺z)))
74	73	2rexbidv 2343	. . . . 5 ⊢ (x = 𝑞 → (∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z) ↔ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)𝑞 = (y𝐺z)))
75		oveq1 5462	. . . . . . 7 ⊢ (y = 𝑟 → (y𝐺z) = (𝑟𝐺z))
76	75	eqeq2d 2048	. . . . . 6 ⊢ (y = 𝑟 → (𝑞 = (y𝐺z) ↔ 𝑞 = (𝑟𝐺z)))
77		oveq2 5463	. . . . . . 7 ⊢ (z = 𝑠 → (𝑟𝐺z) = (𝑟𝐺𝑠))
78	77	eqeq2d 2048	. . . . . 6 ⊢ (z = 𝑠 → (𝑞 = (𝑟𝐺z) ↔ 𝑞 = (𝑟𝐺𝑠)))
79	76, 78	cbvrex2v 2536	. . . . 5 ⊢ (∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)𝑞 = (y𝐺z) ↔ ∃𝑟 ∈ (1^st ‘A)∃𝑠 ∈ (1^st ‘B)𝑞 = (𝑟𝐺𝑠))
80	74, 79	syl6bb 185	. . . 4 ⊢ (x = 𝑞 → (∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z) ↔ ∃𝑟 ∈ (1^st ‘A)∃𝑠 ∈ (1^st ‘B)𝑞 = (𝑟𝐺𝑠)))
81	80	cbvrabv 2550	. . 3 ⊢ {x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^st ‘A)∃𝑠 ∈ (1^st ‘B)𝑞 = (𝑟𝐺𝑠)}
82	73	2rexbidv 2343	. . . . 5 ⊢ (x = 𝑞 → (∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z) ↔ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)𝑞 = (y𝐺z)))
83	76, 78	cbvrex2v 2536	. . . . 5 ⊢ (∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)𝑞 = (y𝐺z) ↔ ∃𝑟 ∈ (2^nd ‘A)∃𝑠 ∈ (2^nd ‘B)𝑞 = (𝑟𝐺𝑠))
84	82, 83	syl6bb 185	. . . 4 ⊢ (x = 𝑞 → (∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z) ↔ ∃𝑟 ∈ (2^nd ‘A)∃𝑠 ∈ (2^nd ‘B)𝑞 = (𝑟𝐺𝑠)))
85	84	cbvrabv 2550	. . 3 ⊢ {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z)} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^nd ‘A)∃𝑠 ∈ (2^nd ‘B)𝑞 = (𝑟𝐺𝑠)}
86	81, 85	opeq12i 3545	. 2 ⊢ ⟨{x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)}, {x ∈ Q ∣ ∃y ∈ (2^nd ‘A)∃z ∈ (2^nd ‘B)x = (y𝐺z)}⟩ = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^st ‘A)∃𝑠 ∈ (1^st ‘B)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^nd ‘A)∃𝑠 ∈ (2^nd ‘B)𝑞 = (𝑟𝐺𝑠)}⟩
87	72, 86	syl6eq 2085	1 ⊢ ((A ∈ P ∧ B ∈ P) → (A𝐹B) = ⟨{𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^st ‘A)∃𝑠 ∈ (1^st ‘B)𝑞 = (𝑟𝐺𝑠)}, {𝑞 ∈ Q ∣ ∃𝑟 ∈ (2^nd ‘A)∃𝑠 ∈ (2^nd ‘B)𝑞 = (𝑟𝐺𝑠)}⟩)

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 884 = wceq 1242 ∈ wcel 1390 {cab 2023 ∃wrex 2301 {crab 2304 Vcvv 2551 ⟨cop 3370 × cxp 4286 ‘cfv 4845 (class class class)co 5455 ↦ cmpt2 5457 1^st c1st 5707 2^nd c2nd 5708 Qcnq 6264 Pcnp 6275

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bndl 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-coll 3863 ax-sep 3866 ax-pow 3918 ax-pr 3935 ax-un 4136 ax-setind 4220 ax-iinf 4254

This theorem depends on definitions: df-bi 110 df-3an 886 df-tru 1245 df-fal 1248 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ne 2203 df-ral 2305 df-rex 2306 df-reu 2307 df-rab 2309 df-v 2553 df-sbc 2759 df-csb 2847 df-dif 2914 df-un 2916 df-in 2918 df-ss 2925 df-pw 3353 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-int 3607 df-iun 3650 df-br 3756 df-opab 3810 df-mpt 3811 df-id 4021 df-iom 4257 df-xp 4294 df-rel 4295 df-cnv 4296 df-co 4297 df-dm 4298 df-rn 4299 df-res 4300 df-ima 4301 df-iota 4810 df-fun 4847 df-fn 4848 df-f 4849 df-f1 4850 df-fo 4851 df-f1o 4852 df-fv 4853 df-ov 5458 df-oprab 5459 df-mpt2 5460 df-1st 5709 df-2nd 5710 df-qs 6048 df-ni 6288 df-nqqs 6332 df-inp 6449

This theorem is referenced by: genpelvl 6495 genpelvu 6496 plpvlu 6521 mpvlu 6522

W3C validator