Theorem genpdflem 7448

Description: Simplification of upper or lower cut expression. Lemma for genpdf 7449. (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 972	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
2	1	rexbii 2473	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
3		r19.42v 2623	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
4	2, 3	bitri 183	. . . . . . . 8 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
5	4	rexbii 2473	. . . . . . 7 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
6		df-rex 2450	. . . . . . 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 1593	. . . . . 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 461	. . . . . 6 ⊢ (𝜑 → ((𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
15	14	exbidv 1813	. . . . 5 ⊢ (𝜑 → (∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
16	10, 15	bitr4id 198	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
17		df-rex 2450	. . . 4 ⊢ (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
18	16, 17	bitr4di 197	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
19		df-rex 2450	. . . . . . 7 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
20		anass 399	. . . . . . . 8 ⊢ (((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
21	20	exbii 1593	. . . . . . 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 461	. . . . . . 7 ⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
27	26	exbidv 1813	. . . . . 6 ⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
28	22, 27	bitr4id 198	. . . . 5 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
29		df-rex 2450	. . . . 5 ⊢ (∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))
30	28, 29	bitr4di 197	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
31	30	rexbidv 2467	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
32	18, 31	bitrd 187	. 2 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
33	32	rabbidv 2715	1 ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)})

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968   = wceq 1343  ∃wex 1480   ∈ wcel 2136  ∃wrex 2445  {crab 2448  (class class class)co 5842  Qcnq 7221

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-ral 2449  df-rex 2450  df-rab 2453

This theorem is referenced by:  genpdf  7449