Theorem genpdflem 7875

Description: Simplification of upper or lower cut expression. Lemma for genpdf 7876. (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 1013	. . . . . . . . . 10 ⊢ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
2	1	rexbii 2557	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
3		r19.42v 2708	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
4	2, 3	bitri 184	. . . . . . . 8 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
5	4	rexbii 2557	. . . . . . 7 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
6		df-rex 2534	. . . . . . 7 ⊢ (∃𝑟 ∈ Q (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
7	5, 6	bitri 184	. . . . . 6 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
8		anass 405	. . . . . . 7 ⊢ (((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ Q ∧ (𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
9	8	exbii 1658	. . . . . 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 398	. . . . . . 7 ⊢ (𝜑 → (𝑟 ∈ 𝐴 ↔ (𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴)))
14	13	anbi1d 469	. . . . . 6 ⊢ (𝜑 → ((𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
15	14	exbidv 1878	. . . . 5 ⊢ (𝜑 → (∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ 𝐴) ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
16	10, 15	bitr4id 199	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))))
17		df-rex 2534	. . . 4 ⊢ (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ 𝐴 ∧ ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
18	16, 17	bitr4di 198	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
19		df-rex 2534	. . . . . . 7 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
20		anass 405	. . . . . . . 8 ⊢ (((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑠 ∈ Q ∧ (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
21	20	exbii 1658	. . . . . . 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 398	. . . . . . . 8 ⊢ (𝜑 → (𝑠 ∈ 𝐵 ↔ (𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵)))
26	25	anbi1d 469	. . . . . . 7 ⊢ (𝜑 → ((𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
27	26	exbidv 1878	. . . . . 6 ⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ 𝐵) ∧ 𝑞 = (𝑟𝐺𝑠))))
28	22, 27	bitr4id 199	. . . . 5 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))))
29		df-rex 2534	. . . . 5 ⊢ (∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠) ↔ ∃𝑠(𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)))
30	28, 29	bitr4di 198	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
31	30	rexbidv 2551	. . 3 ⊢ (𝜑 → (∃𝑟 ∈ 𝐴 ∃𝑠 ∈ Q (𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
32	18, 31	bitrd 188	. 2 ⊢ (𝜑 → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)))
33	32	rabbidv 2810	1 ⊢ (𝜑 → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑞 = (𝑟𝐺𝑠)})

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009   = wceq 1402  ∃wex 1545   ∈ wcel 2209  ∃wrex 2529  {crab 2532  (class class class)co 6085  Qcnq 7648

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-ral 2533  df-rex 2534  df-rab 2537

This theorem is used by:  genpdf  7876