Theorem genpdflem 7591

Description: Simplification of upper or lower cut expression. Lemma for genpdf 7592. (Contributed by Jim Kingdon, 30-Sep-2019.)

Hypotheses

Ref	Expression
genpdflem.r	⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q)
genpdflem.s	⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q)

Assertion

Ref	Expression
genpdflem	⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)})

Distinct variable groups:   𝐴,𝑠   𝜑,𝑞,𝑟,𝑠

Allowed substitution hints:   𝐴(𝑟,𝑞)   𝐵(𝑠,𝑟,𝑞)   𝐺(𝑠,𝑟,𝑞)

Proof of Theorem genpdflem

Step	Hyp	Ref	Expression
1		3anass 984	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
2	1	rexbii 2504	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
3		r19.42v 2654	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
4	2, 3	bitri 184	. . . . . . . 8 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
5	4	rexbii 2504	. . . . . . 7 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
6		df-rex 2481	. . . . . . 7 ⊢ (∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
7	5, 6	bitri 184	. . . . . 6 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
8		anass 401	. . . . . . 7 ⊢ (((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
9	8	exbii 1619	. . . . . 6 ⊢ (∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
10	7, 9	bitr4i 187	. . . . 5 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
11		genpdflem.r	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q)
12	11	ex 115	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ 𝐴 → 𝑟 ∈ Q))
13	12	pm4.71rd 394	. . . . . . 7 ⊢ (𝜑 → (𝑟 ∈ 𝐴 ↔ (𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴)))
14	13	anbi1d 465	. . . . . 6 ⊢ (𝜑 → ((𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
15	14	exbidv 1839	. . . . 5 ⊢ (𝜑 → (∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
16	10, 15	bitr4id 199	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
17		df-rex 2481	. . . 4 ⊢ (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
18	16, 17	bitr4di 198	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
19		df-rex 2481	. . . . . . 7 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
20		anass 401	. . . . . . . 8 ⊢ (((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
21	20	exbii 1619	. . . . . . 7 ⊢ (∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
22	19, 21	bitr4i 187	. . . . . 6 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)))
23		genpdflem.s	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q)
24	23	ex 115	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 ∈ 𝐵 → 𝑠 ∈ Q))
25	24	pm4.71rd 394	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝐵 ↔ (𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵)))
26	25	anbi1d 465	. . . . . . 7 ⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
27	26	exbidv 1839	. . . . . 6 ⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
28	22, 27	bitr4id 199	. . . . 5 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
29		df-rex 2481	. . . . 5 ⊢ (∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))
30	28, 29	bitr4di 198	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
31	30	rexbidv 2498	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
32	18, 31	bitrd 188	. 2 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
33	32	rabbidv 2752	1 ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)})

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 980   = wceq 1364  ∃wex 1506   ∈ wcel 2167  ∃wrex 2476  {crab 2479  (class class class)co 5925  Qcnq 7364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-ral 2480  df-rex 2481  df-rab 2484

This theorem is referenced by:  genpdf  7592