Theorem genpdflem 7690

Description: Simplification of upper or lower cut expression. Lemma for genpdf 7691. (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 1006	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
2	1	rexbii 2537	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
3		r19.42v 2688	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
4	2, 3	bitri 184	. . . . . . . 8 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
5	4	rexbii 2537	. . . . . . 7 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
6		df-rex 2514	. . . . . . 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 1651	. . . . . 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 1871	. . . . 5 ⊢ (𝜑 → (∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
16	10, 15	bitr4id 199	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
17		df-rex 2514	. . . 4 ⊢ (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
18	16, 17	bitr4di 198	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
19		df-rex 2514	. . . . . . 7 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
20		anass 401	. . . . . . . 8 ⊢ (((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
21	20	exbii 1651	. . . . . . 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 1871	. . . . . 6 ⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
28	22, 27	bitr4id 199	. . . . 5 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
29		df-rex 2514	. . . . 5 ⊢ (∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))
30	28, 29	bitr4di 198	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
31	30	rexbidv 2531	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
32	18, 31	bitrd 188	. 2 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
33	32	rabbidv 2788	1 ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)})

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1002   = wceq 1395  ∃wex 1538   ∈ wcel 2200  ∃wrex 2509  {crab 2512  (class class class)co 6000  Qcnq 7463

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-ral 2513  df-rex 2514  df-rab 2517

This theorem is referenced by:  genpdf  7691