Theorem genpdflem 7469

Description: Simplification of upper or lower cut expression. Lemma for genpdf 7470. (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 977	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
2	1	rexbii 2477	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
3		r19.42v 2627	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
4	2, 3	bitri 183	. . . . . . . 8 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
5	4	rexbii 2477	. . . . . . 7 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
6		df-rex 2454	. . . . . . 7 ⊢ (∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
7	5, 6	bitri 183	. . . . . 6 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
8		anass 399	. . . . . . 7 ⊢ (((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
9	8	exbii 1598	. . . . . 6 ⊢ (∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
10	7, 9	bitr4i 186	. . . . 5 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
11		genpdflem.r	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ Q)
12	11	ex 114	. . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ 𝐴 → 𝑟 ∈ Q))
13	12	pm4.71rd 392	. . . . . . 7 ⊢ (𝜑 → (𝑟 ∈ 𝐴 ↔ (𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴)))
14	13	anbi1d 462	. . . . . 6 ⊢ (𝜑 → ((𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
15	14	exbidv 1818	. . . . 5 ⊢ (𝜑 → (∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
16	10, 15	bitr4id 198	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
17		df-rex 2454	. . . 4 ⊢ (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
18	16, 17	bitr4di 197	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
19		df-rex 2454	. . . . . . 7 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
20		anass 399	. . . . . . . 8 ⊢ (((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
21	20	exbii 1598	. . . . . . 7 ⊢ (∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
22	19, 21	bitr4i 186	. . . . . 6 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)))
23		genpdflem.s	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ Q)
24	23	ex 114	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 ∈ 𝐵 → 𝑠 ∈ Q))
25	24	pm4.71rd 392	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝐵 ↔ (𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵)))
26	25	anbi1d 462	. . . . . . 7 ⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
27	26	exbidv 1818	. . . . . 6 ⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
28	22, 27	bitr4id 198	. . . . 5 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
29		df-rex 2454	. . . . 5 ⊢ (∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))
30	28, 29	bitr4di 197	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
31	30	rexbidv 2471	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
32	18, 31	bitrd 187	. 2 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
33	32	rabbidv 2719	1 ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)})

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973   = wceq 1348  ∃wex 1485   ∈ wcel 2141  ∃wrex 2449  {crab 2452  (class class class)co 5853  Qcnq 7242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-ral 2453  df-rex 2454  df-rab 2457

This theorem is referenced by:  genpdf  7470