genipv - Intuitionistic Logic Explorer

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

Theorem genipv 6357

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 5439	. . . 4 ⊢ (f = A → (f𝐹g) = (A𝐹g))
2		fveq2 5099	. . . . . . 7 ⊢ (f = A → (1^st ‘f) = (1^st ‘A))
3	2	rexeqdv 2486	. . . . . 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 2523	. . . . 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 5099	. . . . . . 7 ⊢ (f = A → (2^nd ‘f) = (2^nd ‘A))
6	5	rexeqdv 2486	. . . . . 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 2523	. . . . 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 3527	. . . 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 2032	. . 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 5440	. . . 4 ⊢ (g = B → (A𝐹g) = (A𝐹B))
11		fveq2 5099	. . . . . . . 8 ⊢ (g = B → (1^st ‘g) = (1^st ‘B))
12	11	rexeqdv 2486	. . . . . . 7 ⊢ (g = B → (∃z ∈ (1^st ‘g)x = (y𝐺z) ↔ ∃z ∈ (1^st ‘B)x = (y𝐺z)))
13	12	rexbidv 2301	. . . . . 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 2523	. . . . 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 5099	. . . . . . . 8 ⊢ (g = B → (2^nd ‘g) = (2^nd ‘B))
16	15	rexeqdv 2486	. . . . . . 7 ⊢ (g = B → (∃z ∈ (2^nd ‘g)x = (y𝐺z) ↔ ∃z ∈ (2^nd ‘B)x = (y𝐺z)))
17	16	rexbidv 2301	. . . . . 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 2523	. . . . 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 3527	. . . 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 2032	. . 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 6216	. . . . . . 7 ⊢ Q ∈ V
22	21	a1i 9	. . . . . 6 ⊢ ((f ∈ P ∧ g ∈ P) → Q ∈ V)
23		rabssab 3000	. . . . . . 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 6323	. . . . . . . . . . . 12 ⊢ (f ∈ P → ⟨(1^st ‘f), (2^nd ‘f)⟩ ∈ P)
25		elprnql 6329	. . . . . . . . . . . 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 6323	. . . . . . . . . . . 12 ⊢ (g ∈ P → ⟨(1^st ‘g), (2^nd ‘g)⟩ ∈ P)
28		elprnql 6329	. . . . . . . . . . . 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 2078	. . . . . . . . . . . 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 509	. . . . . . . . 9 ⊢ (((f ∈ P ∧ g ∈ P) ∧ (y ∈ (1^st ‘f) ∧ z ∈ (1^st ‘g))) → (x = (y𝐺z) → x ∈ Q))
35	34	rexlimdvva 2414	. . . . . . . 8 ⊢ ((f ∈ P ∧ g ∈ P) → (∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z) → x ∈ Q))
36	35	abssdv 2987	. . . . . . 7 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ⊆ Q)
37	23, 36	syl5ss 2929	. . . . . 6 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ⊆ Q)
38	22, 37	ssexd 3867	. . . . 5 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (1^st ‘f)∃z ∈ (1^st ‘g)x = (y𝐺z)} ∈ V)
39		rabssab 3000	. . . . . . 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 6330	. . . . . . . . . . . 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 6330	. . . . . . . . . . . 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 509	. . . . . . . . 9 ⊢ (((f ∈ P ∧ g ∈ P) ∧ (y ∈ (2^nd ‘f) ∧ z ∈ (2^nd ‘g))) → (x = (y𝐺z) → x ∈ Q))
46	45	rexlimdvva 2414	. . . . . . . 8 ⊢ ((f ∈ P ∧ g ∈ P) → (∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z) → x ∈ Q))
47	46	abssdv 2987	. . . . . . 7 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ⊆ Q)
48	39, 47	syl5ss 2929	. . . . . 6 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ⊆ Q)
49	22, 48	ssexd 3867	. . . . 5 ⊢ ((f ∈ P ∧ g ∈ P) → {x ∈ Q ∣ ∃y ∈ (2^nd ‘f)∃z ∈ (2^nd ‘g)x = (y𝐺z)} ∈ V)
50		opelxp 4297	. . . . 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 396	. . . 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 5099	. . . . . . . 8 ⊢ (w = f → (1^st ‘w) = (1^st ‘f))
53	52	rexeqdv 2486	. . . . . . 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 2523	. . . . . 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 5099	. . . . . . . 8 ⊢ (w = f → (2^nd ‘w) = (2^nd ‘f))
56	55	rexeqdv 2486	. . . . . . 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 2523	. . . . . 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 3527	. . . . 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 5099	. . . . . . . . 9 ⊢ (v = g → (1^st ‘v) = (1^st ‘g))
60	59	rexeqdv 2486	. . . . . . . 8 ⊢ (v = g → (∃z ∈ (1^st ‘v)x = (y𝐺z) ↔ ∃z ∈ (1^st ‘g)x = (y𝐺z)))
61	60	rexbidv 2301	. . . . . . 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 2523	. . . . . 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 5099	. . . . . . . . 9 ⊢ (v = g → (2^nd ‘v) = (2^nd ‘g))
64	63	rexeqdv 2486	. . . . . . . 8 ⊢ (v = g → (∃z ∈ (2^nd ‘v)x = (y𝐺z) ↔ ∃z ∈ (2^nd ‘g)x = (y𝐺z)))
65	64	rexbidv 2301	. . . . . . 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 2523	. . . . . 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 3527	. . . . 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 6356	. . . . 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 5554	. . . 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 1216	. . 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 2594	. 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 2024	. . . . . 6 ⊢ (x = 𝑞 → (x = (y𝐺z) ↔ 𝑞 = (y𝐺z)))
74	73	2rexbidv 2323	. . . . 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 5439	. . . . . . 7 ⊢ (y = 𝑟 → (y𝐺z) = (𝑟𝐺z))
76	75	eqeq2d 2029	. . . . . 6 ⊢ (y = 𝑟 → (𝑞 = (y𝐺z) ↔ 𝑞 = (𝑟𝐺z)))
77		oveq2 5440	. . . . . . 7 ⊢ (z = 𝑠 → (𝑟𝐺z) = (𝑟𝐺𝑠))
78	77	eqeq2d 2029	. . . . . 6 ⊢ (z = 𝑠 → (𝑞 = (𝑟𝐺z) ↔ 𝑞 = (𝑟𝐺𝑠)))
79	76, 78	cbvrex2v 2516	. . . . 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 2530	. . 3 ⊢ {x ∈ Q ∣ ∃y ∈ (1^st ‘A)∃z ∈ (1^st ‘B)x = (y𝐺z)} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ (1^st ‘A)∃𝑠 ∈ (1^st ‘B)𝑞 = (𝑟𝐺𝑠)}
82	73	2rexbidv 2323	. . . . 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 2516	. . . . 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 2530	. . 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 3524	. 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 2066	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 871 = wceq 1226 ∈ wcel 1370 {cab 2004 ∃wrex 2281 {crab 2284 Vcvv 2531 ⟨cop 3349 × cxp 4266 ‘cfv 4825 (class class class)co 5432 ↦ cmpt2 5434 1^st c1st 5684 2^nd c2nd 5685 Qcnq 6134 Pcnp 6145

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 532 ax-in2 533 ax-io 617 ax-5 1312 ax-7 1313 ax-gen 1314 ax-ie1 1359 ax-ie2 1360 ax-8 1372 ax-10 1373 ax-11 1374 ax-i12 1375 ax-bnd 1376 ax-4 1377 ax-13 1381 ax-14 1382 ax-17 1396 ax-i9 1400 ax-ial 1405 ax-i5r 1406 ax-ext 2000 ax-coll 3842 ax-sep 3845 ax-pow 3897 ax-pr 3914 ax-un 4116 ax-setind 4200 ax-iinf 4234

This theorem depends on definitions: df-bi 110 df-3an 873 df-tru 1229 df-fal 1232 df-nf 1326 df-sb 1624 df-eu 1881 df-mo 1882 df-clab 2005 df-cleq 2011 df-clel 2014 df-nfc 2145 df-ne 2184 df-ral 2285 df-rex 2286 df-reu 2287 df-rab 2289 df-v 2533 df-sbc 2738 df-csb 2826 df-dif 2893 df-un 2895 df-in 2897 df-ss 2904 df-pw 3332 df-sn 3352 df-pr 3353 df-op 3355 df-uni 3551 df-int 3586 df-iun 3629 df-br 3735 df-opab 3789 df-mpt 3790 df-id 4000 df-iom 4237 df-xp 4274 df-rel 4275 df-cnv 4276 df-co 4277 df-dm 4278 df-rn 4279 df-res 4280 df-ima 4281 df-iota 4790 df-fun 4827 df-fn 4828 df-f 4829 df-f1 4830 df-fo 4831 df-f1o 4832 df-fv 4833 df-ov 5435 df-oprab 5436 df-mpt2 5437 df-1st 5686 df-2nd 5687 df-qs 6019 df-ni 6158 df-nqqs 6201 df-inp 6314

This theorem is referenced by: genpelvl 6360 genpelvu 6361 plpvlu 6387 mpvlu 6388

W3C validator