| Step | Hyp | Ref
| Expression |
| 1 | | genp.1 |
. . 3
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)}) |
| 2 | | genp.2 |
. . 3
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) |
| 3 | 1, 2 | genpelv 11040 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑓 ∈ (𝐴𝐹𝐵) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ))) |
| 4 | | prnmax 11035 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 𝑔 <Q 𝑦) |
| 5 | 4 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ∃𝑦 ∈ 𝐴 𝑔 <Q 𝑦) |
| 6 | 1, 2 | genpprecl 11041 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑦 ∈ 𝐴 ∧ ℎ ∈ 𝐵) → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))) |
| 7 | 6 | exp4b 430 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ (𝑦 ∈ 𝐴 → (ℎ ∈ 𝐵 → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))))) |
| 8 | 7 | com34 91 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ (ℎ ∈ 𝐵 → (𝑦 ∈ 𝐴 → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))))) |
| 9 | 8 | imp32 418 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → (𝑦 ∈ 𝐴 → (𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵))) |
| 10 | | elprnq 11031 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → ℎ ∈ Q) |
| 11 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑔 ∈ V |
| 12 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ∈ V |
| 13 | | genpnmax.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ Q →
(𝑧
<Q 𝑤 ↔ (𝑣𝐺𝑧) <Q (𝑣𝐺𝑤))) |
| 14 | | vex 3484 |
. . . . . . . . . . . . . . . 16
⊢ ℎ ∈ V |
| 15 | | genpnmax.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧𝐺𝑤) = (𝑤𝐺𝑧) |
| 16 | 11, 12, 13, 14, 15 | caovord2 7645 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ Q →
(𝑔
<Q 𝑦 ↔ (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
| 17 | 16 | biimpd 229 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ Q →
(𝑔
<Q 𝑦 → (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
| 18 | 10, 17 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ P ∧
ℎ ∈ 𝐵) → (𝑔 <Q 𝑦 → (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
| 19 | 18 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → (𝑔 <Q 𝑦 → (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
| 20 | 9, 19 | anim12d 609 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ ℎ ∈ 𝐵)) → ((𝑦 ∈ 𝐴 ∧ 𝑔 <Q 𝑦) → ((𝑦𝐺ℎ) ∈ (𝐴𝐹𝐵) ∧ (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ)))) |
| 21 | | breq2 5147 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦𝐺ℎ) → ((𝑔𝐺ℎ) <Q 𝑥 ↔ (𝑔𝐺ℎ) <Q (𝑦𝐺ℎ))) |
| 22 | 21 | rspcev 3622 |
. . . . . . . . . . 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 415 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (𝑦 ∈ 𝐴 → (𝑔 <Q 𝑦 → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥))) |
| 26 | 25 | rexlimdv 3153 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → (∃𝑦 ∈ 𝐴 𝑔 <Q 𝑦 → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥)) |
| 27 | 5, 26 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ P ∧
𝑔 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ ℎ ∈ 𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥) |
| 28 | 27 | an4s 660 |
. . . . 5
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥) |
| 29 | | breq1 5146 |
. . . . . 6
⊢ (𝑓 = (𝑔𝐺ℎ) → (𝑓 <Q 𝑥 ↔ (𝑔𝐺ℎ) <Q 𝑥)) |
| 30 | 29 | rexbidv 3179 |
. . . . 5
⊢ (𝑓 = (𝑔𝐺ℎ) → (∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥 ↔ ∃𝑥 ∈ (𝐴𝐹𝐵)(𝑔𝐺ℎ) <Q 𝑥)) |
| 31 | 28, 30 | imbitrrid 246 |
. . . 4
⊢ (𝑓 = (𝑔𝐺ℎ) → (((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧
(𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵)) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥)) |
| 32 | 31 | expdcom 414 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵) → (𝑓 = (𝑔𝐺ℎ) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥))) |
| 33 | 32 | rexlimdvv 3212 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑔 ∈
𝐴 ∃ℎ ∈ 𝐵 𝑓 = (𝑔𝐺ℎ) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥)) |
| 34 | 3, 33 | sylbid 240 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝑓 ∈ (𝐴𝐹𝐵) → ∃𝑥 ∈ (𝐴𝐹𝐵)𝑓 <Q 𝑥)) |