genpelxp - Intuitionistic Logic Explorer

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

Theorem genpelxp 6494

Description: Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)

**Hypothesis**
Ref	Expression
genpelvl.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))}⟩)

**Assertion**
Ref	Expression
genpelxp	⊢ ((A ∈ P ∧ B ∈ P) → (A𝐹B) ∈ (𝒫 Q × 𝒫 Q))

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

**Proof of Theorem genpelxp**
Step	Hyp	Ref	Expression
1		ssrab2 3019	. . . . 5 ⊢ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))} ⊆ Q
2		nqex 6347	. . . . . 6 ⊢ Q ∈ V
3	2	elpw2 3902	. . . . 5 ⊢ ({x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))} ∈ 𝒫 Q ↔ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))} ⊆ Q)
4	1, 3	mpbir 134	. . . 4 ⊢ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))} ∈ 𝒫 Q
5		ssrab2 3019	. . . . 5 ⊢ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))} ⊆ Q
6	2	elpw2 3902	. . . . 5 ⊢ ({x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))} ∈ 𝒫 Q ↔ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))} ⊆ Q)
7	5, 6	mpbir 134	. . . 4 ⊢ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))} ∈ 𝒫 Q
8		opelxpi 4319	. . . 4 ⊢ (({x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))} ∈ 𝒫 Q ∧ {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))} ∈ 𝒫 Q) → ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))}⟩ ∈ (𝒫 Q × 𝒫 Q))
9	4, 7, 8	mp2an 402	. . 3 ⊢ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))}⟩ ∈ (𝒫 Q × 𝒫 Q)
10		fveq2 5121	. . . . . . . . 9 ⊢ (w = A → (1^st ‘w) = (1^st ‘A))
11	10	eleq2d 2104	. . . . . . . 8 ⊢ (w = A → (y ∈ (1^st ‘w) ↔ y ∈ (1^st ‘A)))
12	11	3anbi1d 1210	. . . . . . 7 ⊢ (w = A → ((y ∈ (1^st ‘w) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z)) ↔ (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))))
13	12	2rexbidv 2343	. . . . . 6 ⊢ (w = A → (∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘w) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))))
14	13	rabbidv 2543	. . . . 5 ⊢ (w = A → {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘w) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))} = {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))})
15		fveq2 5121	. . . . . . . . 9 ⊢ (w = A → (2^nd ‘w) = (2^nd ‘A))
16	15	eleq2d 2104	. . . . . . . 8 ⊢ (w = A → (y ∈ (2^nd ‘w) ↔ y ∈ (2^nd ‘A)))
17	16	3anbi1d 1210	. . . . . . 7 ⊢ (w = A → ((y ∈ (2^nd ‘w) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z)) ↔ (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))))
18	17	2rexbidv 2343	. . . . . 6 ⊢ (w = A → (∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘w) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))))
19	18	rabbidv 2543	. . . . 5 ⊢ (w = A → {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘w) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))} = {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))})
20	14, 19	opeq12d 3548	. . . 4 ⊢ (w = A → ⟨{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))}⟩ = ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))}⟩)
21		fveq2 5121	. . . . . . . . 9 ⊢ (v = B → (1^st ‘v) = (1^st ‘B))
22	21	eleq2d 2104	. . . . . . . 8 ⊢ (v = B → (z ∈ (1^st ‘v) ↔ z ∈ (1^st ‘B)))
23	22	3anbi2d 1211	. . . . . . 7 ⊢ (v = B → ((y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z)) ↔ (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))))
24	23	2rexbidv 2343	. . . . . 6 ⊢ (v = B → (∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))))
25	24	rabbidv 2543	. . . . 5 ⊢ (v = B → {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))} = {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))})
26		fveq2 5121	. . . . . . . . 9 ⊢ (v = B → (2^nd ‘v) = (2^nd ‘B))
27	26	eleq2d 2104	. . . . . . . 8 ⊢ (v = B → (z ∈ (2^nd ‘v) ↔ z ∈ (2^nd ‘B)))
28	27	3anbi2d 1211	. . . . . . 7 ⊢ (v = B → ((y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z)) ↔ (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))))
29	28	2rexbidv 2343	. . . . . 6 ⊢ (v = B → (∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z)) ↔ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))))
30	29	rabbidv 2543	. . . . 5 ⊢ (v = B → {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))} = {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))})
31	25, 30	opeq12d 3548	. . . 4 ⊢ (v = B → ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘v) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘v) ∧ x = (y𝐺z))}⟩ = ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))}⟩)
32		genpelvl.1	. . . 4 ⊢ 𝐹 = (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))}⟩)
33	20, 31, 32	ovmpt2g 5577	. . 3 ⊢ ((A ∈ P ∧ B ∈ P ∧ ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))}⟩ ∈ (𝒫 Q × 𝒫 Q)) → (A𝐹B) = ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))}⟩)
34	9, 33	mp3an3 1220	. 2 ⊢ ((A ∈ P ∧ B ∈ P) → (A𝐹B) = ⟨{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (1^st ‘A) ∧ z ∈ (1^st ‘B) ∧ x = (y𝐺z))}, {x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈ (2^nd ‘A) ∧ z ∈ (2^nd ‘B) ∧ x = (y𝐺z))}⟩)
35	34, 9	syl6eqel 2125	1 ⊢ ((A ∈ P ∧ B ∈ P) → (A𝐹B) ∈ (𝒫 Q × 𝒫 Q))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 97 ∧ w3a 884 = wceq 1242 ∈ wcel 1390 ∃wrex 2301 {crab 2304 ⊆ wss 2911 𝒫 cpw 3351 ⟨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-qs 6048 df-ni 6288 df-nqqs 6332

This theorem is referenced by: addclpr 6520 mulclpr 6553

W3C validator