Step | Hyp | Ref
| Expression |
1 | | elxp 5542 |
. . . . . . . 8
⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵))) |
2 | | elxp 5542 |
. . . . . . . 8
⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵))) |
3 | | elxp 5542 |
. . . . . . . 8
⊢ (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒∃𝑓(𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) |
4 | | 3an6 1447 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) ↔ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)))) |
5 | | poirr 5449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 Po 𝐴 ∧ 𝑎 ∈ 𝐴) → ¬ 𝑎𝑅𝑎) |
6 | 5 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑅 Po 𝐴 → (𝑎 ∈ 𝐴 → ¬ 𝑎𝑅𝑎)) |
7 | | poirr 5449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏𝑆𝑏) |
8 | 7 | intnand 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) |
9 | 8 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 Po 𝐵 → (𝑏 ∈ 𝐵 → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) |
10 | 6, 9 | im2anan9 623 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
11 | | ioran 983 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) |
12 | 10, 11 | syl6ibr 255 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
13 | 12 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) |
14 | 13 | intnand 492 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
15 | 14 | 3ad2antr1 1189 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
16 | | an4 656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))))) |
17 | | 3an6 1447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) |
18 | | potr 5450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → 𝑎𝑅𝑒)) |
19 | 18 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → 𝑎𝑅𝑒) |
20 | 19 | orcd 872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))) |
21 | 20 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
22 | 21 | expdimp 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
23 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 = 𝑒 → (𝑎𝑅𝑐 ↔ 𝑎𝑅𝑒)) |
24 | 23 | biimpa 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → 𝑎𝑅𝑒) |
25 | 24 | orcd 872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))) |
26 | 25 | expcom 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
27 | 26 | adantrd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎𝑅𝑐 → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
28 | 27 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
29 | 22, 28 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
30 | 29 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
31 | | potr 5450 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑏𝑆𝑑 ∧ 𝑑𝑆𝑓) → 𝑏𝑆𝑓)) |
32 | 31 | expdimp 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓 → 𝑏𝑆𝑓)) |
33 | 32 | anim2d 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))) |
34 | 33 | orim2d 966 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
35 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 = 𝑐 → (𝑎𝑅𝑒 ↔ 𝑐𝑅𝑒)) |
36 | | equequ1 2036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 = 𝑐 → (𝑎 = 𝑒 ↔ 𝑐 = 𝑒)) |
37 | 36 | anbi1d 633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 = 𝑐 → ((𝑎 = 𝑒 ∧ 𝑏𝑆𝑓) ↔ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))) |
38 | 35, 37 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
39 | 38 | imbi2d 344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
40 | 34, 39 | syl5ibr 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
41 | 40 | expd 419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))) |
42 | 41 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))) |
43 | 42 | impd 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
44 | 30, 43 | jaao 954 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
45 | 44 | impd 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
46 | 45 | an4s 660 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
47 | 17, 46 | sylan2b 597 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
48 | | an4 656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) |
49 | 48 | biimpi 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) |
50 | 49 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) |
51 | 50 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) |
52 | 47, 51 | jctild 529 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
53 | 52 | adantld 494 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
54 | 16, 53 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
55 | 15, 54 | jca 515 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))) |
56 | | breq12 5032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑡 = 〈𝑎, 𝑏〉) → (𝑡𝑇𝑡 ↔ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
57 | 56 | anidms 570 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡𝑇𝑡 ↔ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
58 | 57 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (¬ 𝑡𝑇𝑡 ↔ ¬ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
59 | 58 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (¬ 𝑡𝑇𝑡 ↔ ¬ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
60 | | breq12 5032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉) → (𝑡𝑇𝑢 ↔ 〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉)) |
61 | 60 | 3adant3 1133 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (𝑡𝑇𝑢 ↔ 〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉)) |
62 | | breq12 5032 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (𝑢𝑇𝑣 ↔ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉)) |
63 | 62 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (𝑢𝑇𝑣 ↔ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉)) |
64 | 61, 63 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) ↔ (〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉))) |
65 | | breq12 5032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (𝑡𝑇𝑣 ↔ 〈𝑎, 𝑏〉𝑇〈𝑒, 𝑓〉)) |
66 | 65 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (𝑡𝑇𝑣 ↔ 〈𝑎, 𝑏〉𝑇〈𝑒, 𝑓〉)) |
67 | 64, 66 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, 𝑓〉))) |
68 | 59, 67 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ∧ ((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, 𝑓〉)))) |
69 | | poxp.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1st ‘𝑥)𝑅(1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥)𝑆(2nd ‘𝑦))))} |
70 | 69 | xporderlem 7840 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ↔ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
71 | 70 | notbii 323 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ↔ ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
72 | 69 | xporderlem 7840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))) |
73 | 69 | xporderlem 7840 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉 ↔ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) |
74 | 72, 73 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))))) |
75 | 69 | xporderlem 7840 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉𝑇〈𝑒, 𝑓〉 ↔ (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))) |
76 | 74, 75 | imbi12i 354 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, 𝑓〉) ↔ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))) |
77 | 71, 76 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ∧ ((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧ 〈𝑐, 𝑑〉𝑇〈𝑒, 𝑓〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, 𝑓〉)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))) |
78 | 68, 77 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))) |
79 | 55, 78 | syl5ibr 249 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))) |
80 | 79 | expcomd 420 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))) |
81 | 80 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 = 〈𝑎, 𝑏〉 ∧ 𝑢 = 〈𝑐, 𝑑〉 ∧ 𝑣 = 〈𝑒, 𝑓〉) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))) |
82 | 4, 81 | sylbi 220 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))) |
83 | 82 | 3exp 1120 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))) |
84 | 83 | com3l 89 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))) |
85 | 84 | exlimivv 1938 |
. . . . . . . . . . . . 13
⊢
(∃𝑐∃𝑑(𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))) |
86 | 85 | com3l 89 |
. . . . . . . . . . . 12
⊢ ((𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))) |
87 | 86 | exlimivv 1938 |
. . . . . . . . . . 11
⊢
(∃𝑒∃𝑓(𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))) |
88 | 87 | com3l 89 |
. . . . . . . . . 10
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))) |
89 | 88 | exlimivv 1938 |
. . . . . . . . 9
⊢
(∃𝑎∃𝑏(𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))) |
90 | 89 | 3imp 1112 |
. . . . . . . 8
⊢
((∃𝑎∃𝑏(𝑡 = 〈𝑎, 𝑏〉 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ ∃𝑒∃𝑓(𝑣 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))) |
91 | 1, 2, 3, 90 | syl3anb 1162 |
. . . . . . 7
⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))) |
92 | 91 | 3expia 1122 |
. . . . . 6
⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))) |
93 | 92 | com3r 87 |
. . . . 5
⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))) |
94 | 93 | imp 410 |
. . . 4
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))) |
95 | 94 | ralrimiv 3095 |
. . 3
⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))) |
96 | 95 | ralrimivva 3103 |
. 2
⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))) |
97 | | df-po 5438 |
. 2
⊢ (𝑇 Po (𝐴 × 𝐵) ↔ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))) |
98 | 96, 97 | sylibr 237 |
1
⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵)) |