Theorem genpdflem 6490

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

Hypotheses

Ref	Expression
genpdflem.r	⊢ ((φ ∧ 𝑟 ∈ A) → 𝑟 ∈ Q)
genpdflem.s	⊢ ((φ ∧ 𝑠 ∈ B) → 𝑠 ∈ Q)

Assertion

Ref	Expression
genpdflem	⊢ (φ → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ A ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠)})

Distinct variable groups:   A,𝑠   φ,𝑞,𝑟,𝑠

Allowed substitution hints:   A(𝑟,𝑞)   B(𝑠,𝑟,𝑞)   𝐺(𝑠,𝑟,𝑞)

Proof of Theorem genpdflem

Step	Hyp	Ref	Expression
1		genpdflem.r	. . . . . . . . 9 ⊢ ((φ ∧ 𝑟 ∈ A) → 𝑟 ∈ Q)
2	1	ex 108	. . . . . . . 8 ⊢ (φ → (𝑟 ∈ A → 𝑟 ∈ Q))
3	2	pm4.71rd 374	. . . . . . 7 ⊢ (φ → (𝑟 ∈ A ↔ (𝑟 ∈ Q ∧ 𝑟 ∈ A)))
4	3	anbi1d 438	. . . . . 6 ⊢ (φ → ((𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ((𝑟 ∈ Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))))
5	4	exbidv 1703	. . . . 5 ⊢ (φ → (∃𝑟(𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))))
6		3anass 888	. . . . . . . . . 10 ⊢ ((𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ A ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
7	6	rexbii 2325	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ Q (𝑟 ∈ A ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
8		r19.42v 2461	. . . . . . . . 9 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ A ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
9	7, 8	bitri 173	. . . . . . . 8 ⊢ (∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
10	9	rexbii 2325	. . . . . . 7 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ Q (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
11		df-rex 2306	. . . . . . 7 ⊢ (∃𝑟 ∈ Q (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))))
12	10, 11	bitri 173	. . . . . 6 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))))
13		anass 381	. . . . . . 7 ⊢ (((𝑟 ∈ Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ (𝑟 ∈ Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))))
14	13	exbii 1493	. . . . . 6 ⊢ (∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))) ↔ ∃𝑟(𝑟 ∈ Q ∧ (𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))))
15	12, 14	bitr4i 176	. . . . 5 ⊢ (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟((𝑟 ∈ Q ∧ 𝑟 ∈ A) ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
16	5, 15	syl6rbbr 188	. . . 4 ⊢ (φ → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))))
17		df-rex 2306	. . . 4 ⊢ (∃𝑟 ∈ A ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟(𝑟 ∈ A ∧ ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
18	16, 17	syl6bbr 187	. . 3 ⊢ (φ → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ A ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
19		genpdflem.s	. . . . . . . . . 10 ⊢ ((φ ∧ 𝑠 ∈ B) → 𝑠 ∈ Q)
20	19	ex 108	. . . . . . . . 9 ⊢ (φ → (𝑠 ∈ B → 𝑠 ∈ Q))
21	20	pm4.71rd 374	. . . . . . . 8 ⊢ (φ → (𝑠 ∈ B ↔ (𝑠 ∈ Q ∧ 𝑠 ∈ B)))
22	21	anbi1d 438	. . . . . . 7 ⊢ (φ → ((𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ((𝑠 ∈ Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠))))
23	22	exbidv 1703	. . . . . 6 ⊢ (φ → (∃𝑠(𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠))))
24		df-rex 2306	. . . . . . 7 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
25		anass 381	. . . . . . . 8 ⊢ (((𝑠 ∈ Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ (𝑠 ∈ Q ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
26	25	exbii 1493	. . . . . . 7 ⊢ (∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ Q ∧ (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
27	24, 26	bitr4i 176	. . . . . 6 ⊢ (∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠((𝑠 ∈ Q ∧ 𝑠 ∈ B) ∧ 𝑞 = (𝑟𝐺𝑠)))
28	23, 27	syl6rbbr 188	. . . . 5 ⊢ (φ → (∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠(𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))))
29		df-rex 2306	. . . . 5 ⊢ (∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠) ↔ ∃𝑠(𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)))
30	28, 29	syl6bbr 187	. . . 4 ⊢ (φ → (∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠)))
31	30	rexbidv 2321	. . 3 ⊢ (φ → (∃𝑟 ∈ A ∃𝑠 ∈ Q (𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ A ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠)))
32	18, 31	bitrd 177	. 2 ⊢ (φ → (∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠)) ↔ ∃𝑟 ∈ A ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠)))
33	32	rabbidv 2543	1 ⊢ (φ → {𝑞 ∈ Q ∣ ∃𝑟 ∈ Q ∃𝑠 ∈ Q (𝑟 ∈ A ∧ 𝑠 ∈ B ∧ 𝑞 = (𝑟𝐺𝑠))} = {𝑞 ∈ Q ∣ ∃𝑟 ∈ A ∃𝑠 ∈ B 𝑞 = (𝑟𝐺𝑠)})

Syntax hints:   → wi 4   ∧ wa 97   ∧ w3a 884   = wceq 1242  ∃wex 1378   ∈ wcel 1390  ∃wrex 2301  {crab 2304  (class class class)co 5455  Qcnq 6264

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-ral 2305  df-rex 2306  df-rab 2309

This theorem is referenced by:  genpdf  6491