Step | Hyp | Ref
| Expression |
1 | | genp.1 |
. . 3
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)}) |
2 | | genp.2 |
. . 3
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) |
3 | 1, 2 | genpelv 10614 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑓 ∈ (𝐴𝐹𝐵) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ))) |
4 | | prnmax 10609 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 𝑔 <Q 𝑦) |
5 | 4 | adantr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ∃𝑦 ∈ 𝐴 𝑔 <Q 𝑦) |
6 | 1, 2 | genpprecl 10615 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑦 ∈ 𝐴 ∧ ℎ ∈ 𝐵) → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))) |
7 | 6 | exp4b 434 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ (𝑦 ∈ 𝐴 → (ℎ ∈ 𝐵 → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))))) |
8 | 7 | com34 91 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ (ℎ ∈ 𝐵 → (𝑦 ∈ 𝐴 → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))))) |
9 | 8 | imp32 422 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → (𝑦 ∈ 𝐴 → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))) |
10 | | elprnq 10605 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → ℎ ∈ Q) |
11 | | vex 3412 |
. . . . . . . . . . . . . . . 16
⊢ 𝑔 ∈ V |
12 | | vex 3412 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
13 | | genpnmax.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ Q →
(𝑧
<Q 𝑤 ↔ (𝑣𝐺𝑧) <Q (𝑣𝐺𝑤))) |
14 | | vex 3412 |
. . . . . . . . . . . . . . . 16
⊢ ℎ ∈ V |
15 | | genpnmax.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧𝐺𝑤) = (𝑤𝐺𝑧) |
16 | 11, 12, 13, 14, 15 | caovord2 7420 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ Q →
(𝑔
<Q 𝑦 ↔ (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
17 | 16 | biimpd 232 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ Q →
(𝑔
<Q 𝑦 → (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
18 | 10, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → (𝑔 <Q 𝑦 → (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
19 | 18 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → (𝑔 <Q 𝑦 → (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
20 | 9, 19 | anim12d 612 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → ((𝑦 ∈ 𝐴 ∧ 𝑔 <Q 𝑦) → ((𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵) ∧ (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ)))) |
21 | | breq2 5057 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦𝐺ℎ) → ((𝑔𝐺ℎ) <Q 𝑥 ↔ (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
22 | 21 | rspcev 3537 |
. . . . . . . . . . 11
⊢ (((𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵) ∧ (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥) |
23 | 20, 22 | syl6 35 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → ((𝑦 ∈ 𝐴 ∧ 𝑔 <Q 𝑦) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥)) |
24 | 23 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ((𝑦 ∈ 𝐴 ∧ 𝑔 <Q 𝑦) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥)) |
25 | 24 | expd 419 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑦 ∈ 𝐴 → (𝑔 <Q 𝑦 → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥))) |
26 | 25 | rexlimdv 3202 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (∃𝑦 ∈ 𝐴 𝑔 <Q 𝑦 → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥)) |
27 | 5, 26 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥) |
28 | 27 | an4s 660 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥) |
29 | | breq1 5056 |
. . . . . 6
⊢ (𝑓 = (𝑔𝐺ℎ) → (𝑓 <Q 𝑥 ↔ (𝑔𝐺ℎ) <Q 𝑥)) |
30 | 29 | rexbidv 3216 |
. . . . 5
⊢ (𝑓 = (𝑔𝐺ℎ) → (∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥 ↔ ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥)) |
31 | 28, 30 | syl5ibr 249 |
. . . 4
⊢ (𝑓 = (𝑔𝐺ℎ) → (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧
(𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥)) |
32 | 31 | expdcom 418 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵) → (𝑓 = (𝑔𝐺ℎ) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥))) |
33 | 32 | rexlimdvv 3212 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑔 ∈
𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥)) |
34 | 3, 33 | sylbid 243 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑓 ∈ (𝐴𝐹𝐵) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥)) |