Step | Hyp | Ref
| Expression |
1 | | prpssnq 10747 |
. . . . 5
⊢ (𝐴 ∈ P →
𝐴 ⊊
Q) |
2 | | pssnel 4410 |
. . . . 5
⊢ (𝐴 ⊊ Q →
∃𝑤(𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴)) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐴 ∈ P →
∃𝑤(𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴)) |
4 | | prpssnq 10747 |
. . . . 5
⊢ (𝐵 ∈ P →
𝐵 ⊊
Q) |
5 | | pssnel 4410 |
. . . . 5
⊢ (𝐵 ⊊ Q →
∃𝑣(𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵)) |
6 | 4, 5 | syl 17 |
. . . 4
⊢ (𝐵 ∈ P →
∃𝑣(𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵)) |
7 | 3, 6 | anim12i 613 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑤(𝑤 ∈ Q ∧
¬ 𝑤 ∈ 𝐴) ∧ ∃𝑣(𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵))) |
8 | | exdistrv 1963 |
. . 3
⊢
(∃𝑤∃𝑣((𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵)) ↔ (∃𝑤(𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴) ∧ ∃𝑣(𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵))) |
9 | 7, 8 | sylibr 233 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ∃𝑤∃𝑣((𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵))) |
10 | | prub 10751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑤 ∈ Q) → (¬ 𝑤 ∈ 𝐴 → 𝑓 <Q 𝑤)) |
11 | | prub 10751 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ P ∧
𝑔 ∈ 𝐵) ∧ 𝑣 ∈ Q) → (¬ 𝑣 ∈ 𝐵 → 𝑔 <Q 𝑣)) |
12 | 10, 11 | im2anan9 620 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑤 ∈ Q) ∧ ((𝐵 ∈ P ∧
𝑔 ∈ 𝐵) ∧ 𝑣 ∈ Q)) → ((¬
𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵) → (𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣))) |
13 | | elprnq 10748 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) → 𝑓 ∈ Q) |
14 | 13 | anim1i 615 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑤 ∈ Q) → (𝑓 ∈ Q ∧
𝑤 ∈
Q)) |
15 | | elprnq 10748 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ P ∧
𝑔 ∈ 𝐵) → 𝑔 ∈ Q) |
16 | 15 | anim1i 615 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ P ∧
𝑔 ∈ 𝐵) ∧ 𝑣 ∈ Q) → (𝑔 ∈ Q ∧
𝑣 ∈
Q)) |
17 | | ltsonq 10726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
<Q Or Q |
18 | | so2nr 5530 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((
<Q Or Q ∧ (𝑓 ∈ Q ∧ 𝑤 ∈ Q)) →
¬ (𝑓
<Q 𝑤 ∧ 𝑤 <Q 𝑓)) |
19 | 17, 18 | mpan 687 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓 ∈ Q ∧
𝑤 ∈ Q)
→ ¬ (𝑓
<Q 𝑤 ∧ 𝑤 <Q 𝑓)) |
20 | 19 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑓 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑔 ∈
Q ∧ 𝑣
∈ Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓)) |
21 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑔 ∈ Q ∧
𝑣 ∈ Q)
→ 𝑣 ∈
Q) |
22 | | simpl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓 ∈ Q ∧
𝑤 ∈ Q)
→ 𝑓 ∈
Q) |
23 | 21, 22 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑔 ∈ Q ∧
𝑣 ∈ Q)
∧ (𝑓 ∈
Q ∧ 𝑤
∈ Q)) → (𝑣 ∈ Q ∧ 𝑓 ∈
Q)) |
24 | 23 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑔 ∈
Q ∧ 𝑣
∈ Q)) → (𝑣 ∈ Q ∧ 𝑓 ∈
Q)) |
25 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑤 ∈ V |
26 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑣 ∈ V |
27 | | genpnnp.3 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑧 ∈ Q →
(𝑥
<Q 𝑦 ↔ (𝑧𝐺𝑥) <Q (𝑧𝐺𝑦))) |
28 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑓 ∈ V |
29 | | genpnnp.4 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥𝐺𝑦) = (𝑦𝐺𝑥) |
30 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑔 ∈ V |
31 | 25, 26, 27, 28, 29, 30 | caovord3 7479 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑣 ∈ Q ∧
𝑓 ∈ Q)
∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → (𝑤 <Q 𝑓 ↔ 𝑔 <Q 𝑣)) |
32 | 31 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑣 ∈ Q ∧
𝑓 ∈ Q)
∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣))) |
33 | 24, 32 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑓 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑔 ∈
Q ∧ 𝑣
∈ Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ((𝑓 <Q 𝑤 ∧ 𝑤 <Q 𝑓) ↔ (𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣))) |
34 | 20, 33 | mtbid 324 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑓 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑔 ∈
Q ∧ 𝑣
∈ Q)) ∧ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) → ¬ (𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣)) |
35 | 34 | ex 413 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑔 ∈
Q ∧ 𝑣
∈ Q)) → ((𝑤𝐺𝑣) = (𝑓𝐺𝑔) → ¬ (𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣))) |
36 | 35 | con2d 134 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓 ∈ Q ∧
𝑤 ∈ Q)
∧ (𝑔 ∈
Q ∧ 𝑣
∈ Q)) → ((𝑓 <Q 𝑤 ∧ 𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))) |
37 | 14, 16, 36 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑤 ∈ Q) ∧ ((𝐵 ∈ P ∧
𝑔 ∈ 𝐵) ∧ 𝑣 ∈ Q)) → ((𝑓 <Q
𝑤 ∧ 𝑔 <Q 𝑣) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))) |
38 | 12, 37 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ 𝑤 ∈ Q) ∧ ((𝐵 ∈ P ∧
𝑔 ∈ 𝐵) ∧ 𝑣 ∈ Q)) → ((¬
𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))) |
39 | 38 | an4s 657 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ 𝑔 ∈ 𝐵)) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)) →
((¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))) |
40 | 39 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ P ∧
𝑓 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ 𝑔 ∈ 𝐵)) → ((𝑤 ∈ Q ∧ 𝑣 ∈ Q) →
((¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))) |
41 | 40 | an4s 657 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵)) → ((𝑤 ∈ Q ∧ 𝑣 ∈ Q) →
((¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)))) |
42 | 41 | ex 413 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵) → ((𝑤 ∈ Q ∧ 𝑣 ∈ Q) →
((¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))) |
43 | 42 | com24 95 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((¬ 𝑤 ∈
𝐴 ∧ ¬ 𝑣 ∈ 𝐵) → ((𝑤 ∈ Q ∧ 𝑣 ∈ Q) →
((𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))))) |
44 | 43 | imp32 419 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ((¬ 𝑤 ∈
𝐴 ∧ ¬ 𝑣 ∈ 𝐵) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)))
→ ((𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐵) → ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔))) |
45 | 44 | ralrimivv 3116 |
. . . . . . . . 9
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ((¬ 𝑤 ∈
𝐴 ∧ ¬ 𝑣 ∈ 𝐵) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)))
→ ∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) |
46 | | ralnex2 3191 |
. . . . . . . . 9
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐵 ¬ (𝑤𝐺𝑣) = (𝑓𝐺𝑔) ↔ ¬ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) |
47 | 45, 46 | sylib 217 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ((¬ 𝑤 ∈
𝐴 ∧ ¬ 𝑣 ∈ 𝐵) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)))
→ ¬ ∃𝑓
∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔)) |
48 | | genp.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑤 ∈ P, 𝑣 ∈ P ↦ {𝑥 ∣ ∃𝑦 ∈ 𝑤 ∃𝑧 ∈ 𝑣 𝑥 = (𝑦𝐺𝑧)}) |
49 | | genp.2 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦𝐺𝑧) ∈ Q) |
50 | 48, 49 | genpelv 10757 |
. . . . . . . . 9
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))) |
51 | 50 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ((¬ 𝑤 ∈
𝐴 ∧ ¬ 𝑣 ∈ 𝐵) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)))
→ ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ ∃𝑓 ∈ 𝐴 ∃𝑔 ∈ 𝐵 (𝑤𝐺𝑣) = (𝑓𝐺𝑔))) |
52 | 47, 51 | mtbird 325 |
. . . . . . 7
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ ((¬ 𝑤 ∈
𝐴 ∧ ¬ 𝑣 ∈ 𝐵) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)))
→ ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵)) |
53 | 52 | expcom 414 |
. . . . . 6
⊢ (((¬
𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵) ∧ (𝑤 ∈ Q ∧ 𝑣 ∈ Q)) →
((𝐴 ∈ P
∧ 𝐵 ∈
P) → ¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))) |
54 | 53 | ancoms 459 |
. . . . 5
⊢ (((𝑤 ∈ Q ∧
𝑣 ∈ Q)
∧ (¬ 𝑤 ∈ 𝐴 ∧ ¬ 𝑣 ∈ 𝐵)) → ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))) |
55 | 54 | an4s 657 |
. . . 4
⊢ (((𝑤 ∈ Q ∧
¬ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵)) → ((𝐴 ∈ P ∧ 𝐵 ∈ P) →
¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))) |
56 | 49 | caovcl 7460 |
. . . . . 6
⊢ ((𝑤 ∈ Q ∧
𝑣 ∈ Q)
→ (𝑤𝐺𝑣) ∈ Q) |
57 | | eleq2 2829 |
. . . . . . . 8
⊢ ((𝐴𝐹𝐵) = Q → ((𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) ↔ (𝑤𝐺𝑣) ∈ Q)) |
58 | 57 | biimprcd 249 |
. . . . . . 7
⊢ ((𝑤𝐺𝑣) ∈ Q → ((𝐴𝐹𝐵) = Q → (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵))) |
59 | 58 | con3d 152 |
. . . . . 6
⊢ ((𝑤𝐺𝑣) ∈ Q → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q)) |
60 | 56, 59 | syl 17 |
. . . . 5
⊢ ((𝑤 ∈ Q ∧
𝑣 ∈ Q)
→ (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q)) |
61 | 60 | ad2ant2r 744 |
. . . 4
⊢ (((𝑤 ∈ Q ∧
¬ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵)) → (¬ (𝑤𝐺𝑣) ∈ (𝐴𝐹𝐵) → ¬ (𝐴𝐹𝐵) = Q)) |
62 | 55, 61 | syldc 48 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (((𝑤 ∈
Q ∧ ¬ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵)) → ¬ (𝐴𝐹𝐵) = Q)) |
63 | 62 | exlimdvv 1941 |
. 2
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑤∃𝑣((𝑤 ∈ Q ∧ ¬ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ Q ∧ ¬ 𝑣 ∈ 𝐵)) → ¬ (𝐴𝐹𝐵) = Q)) |
64 | 9, 63 | mpd 15 |
1
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ¬ (𝐴𝐹𝐵) = Q) |