Step | Hyp | Ref
| Expression |
1 | | elxp 4305 |
. . . . . . . 8
⊢ (𝑡 ∈ (A ×
B) ↔ ∃𝑎∃𝑏(𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))) |
2 | | elxp 4305 |
. . . . . . . 8
⊢ (u ∈ (A × B)
↔ ∃𝑐∃𝑑(u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))) |
3 | | elxp 4305 |
. . . . . . . 8
⊢ (v ∈ (A × B)
↔ ∃𝑒∃f(v =
〈𝑒, f〉 ∧ (𝑒 ∈ A ∧ f ∈ B))) |
4 | | 3an6 1216 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
∧ (u =
〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
∧ (v =
〈𝑒, f〉 ∧ (𝑒 ∈ A ∧ f ∈ B))) ↔
((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)))) |
5 | | poirr 4035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 Po A ∧ 𝑎 ∈ A) → ¬ 𝑎𝑅𝑎) |
6 | 5 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑅 Po A → (𝑎 ∈ A → ¬ 𝑎𝑅𝑎)) |
7 | | poirr 4035 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 Po B ∧ 𝑏 ∈ B) → ¬ 𝑏𝑆𝑏) |
8 | 7 | intnand 839 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑆 Po B ∧ 𝑏 ∈ B) → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) |
9 | 8 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑆 Po B → (𝑏 ∈ B → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) |
10 | 6, 9 | im2anan9 530 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ((𝑎 ∈ A ∧ 𝑏 ∈ B) → (¬ 𝑎𝑅𝑎 ∧ ¬
(𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
11 | | ioran 668 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (¬
(𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬
(𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) |
12 | 10, 11 | syl6ibr 151 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ((𝑎 ∈ A ∧ 𝑏 ∈ B) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
13 | 12 | imp 115 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑎 ∈ A ∧ 𝑏
∈ B))
→ ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) |
14 | 13 | intnand 839 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑎 ∈ A ∧ 𝑏
∈ B))
→ ¬ (((𝑎 ∈ A ∧ 𝑎
∈ A)
∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
15 | 14 | 3ad2antr1 1068 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
¬ (((𝑎 ∈ A ∧ 𝑎
∈ A)
∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
16 | | an4 520 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝑎 ∈ A ∧ 𝑐
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧
(((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
↔ ((((𝑎 ∈ A ∧ 𝑐
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ ((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))) |
17 | | 3an6 1216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)) ↔
((𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B))) |
18 | | potr 4036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
→ ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → 𝑎𝑅𝑒)) |
19 | 18 | 3impia 1100 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A)
∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → 𝑎𝑅𝑒) |
20 | 19 | orcd 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A)
∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))) |
21 | 20 | 3expia 1105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
→ ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
22 | 21 | expdimp 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
23 | | breq2 3759 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑐 = 𝑒 → (𝑎𝑅𝑐 ↔ 𝑎𝑅𝑒)) |
24 | 23 | biimpa 280 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → 𝑎𝑅𝑒) |
25 | 24 | orcd 651 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))) |
26 | 25 | expcom 109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
27 | 26 | adantrd 264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎𝑅𝑐 → ((𝑐 = 𝑒 ∧ 𝑑𝑆f)
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
28 | 27 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒 ∧ 𝑑𝑆f)
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
29 | 22, 28 | jaod 636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
30 | 29 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
→ (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
31 | | potr 4036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑
∈ B ∧ f ∈ B)) →
((𝑏𝑆𝑑 ∧ 𝑑𝑆f)
→ 𝑏𝑆f)) |
32 | 31 | expdimp 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑
∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆f →
𝑏𝑆f)) |
33 | 32 | anim2d 320 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑
∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒 ∧ 𝑑𝑆f)
→ (𝑐 = 𝑒 ∧ 𝑏𝑆f))) |
34 | 33 | orim2d 701 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑
∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆f)))) |
35 | | breq1 3758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 = 𝑐 → (𝑎𝑅𝑒 ↔ 𝑐𝑅𝑒)) |
36 | | equequ1 1595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑎 = 𝑐 → (𝑎 = 𝑒 ↔ 𝑐 = 𝑒)) |
37 | 36 | anbi1d 438 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑎 = 𝑐 → ((𝑎 = 𝑒 ∧ 𝑏𝑆f)
↔ (𝑐 = 𝑒 ∧ 𝑏𝑆f))) |
38 | 35, 37 | orbi12d 706 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))
↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆f)))) |
39 | 38 | imbi2d 219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))
↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆f))))) |
40 | 34, 39 | syl5ibr 145 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 = 𝑐 → (((𝑆 Po B
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
41 | 40 | expd 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑎 = 𝑐 → ((𝑆 Po B
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))) |
42 | 41 | com12 27 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑
∈ B ∧ f ∈ B)) →
(𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))) |
43 | 42 | impd 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑
∈ B ∧ f ∈ B)) →
((𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
44 | 30, 43 | jaao 638 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
∧ (𝑆 Po B
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
45 | 44 | impd 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A))
∧ (𝑆 Po B
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
46 | 45 | an4s 522 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑐
∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
47 | 17, 46 | sylan2b 271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
(((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))
→ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
48 | | an4 520 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑒 ∈ A ∧ f ∈ B)) ↔ ((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B))) |
49 | 48 | biimpi 113 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B))) |
50 | 49 | 3adant2 922 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)) →
((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B))) |
51 | 50 | adantl 262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B))) |
52 | 47, 51 | jctild 299 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
(((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))
→ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
53 | 52 | adantld 263 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
(((((𝑎 ∈ A ∧ 𝑐
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ ((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
→ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
54 | 16, 53 | syl5bi 141 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
(((((𝑎 ∈ A ∧ 𝑐
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧
(((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
→ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
55 | 15, 54 | jca 290 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
(¬ (((𝑎 ∈ A ∧ 𝑎
∈ A)
∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧
(((((𝑎 ∈ A ∧ 𝑐
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧
(((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
→ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))) |
56 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
𝑡 = 〈𝑎, 𝑏〉) → (𝑡𝑇𝑡 ↔ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
57 | 56 | anidms 377 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (𝑡𝑇𝑡 ↔ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
58 | 57 | notbid 591 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑡 = 〈𝑎, 𝑏〉 → (¬ 𝑡𝑇𝑡 ↔ ¬ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
59 | 58 | 3ad2ant1 924 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (¬ 𝑡𝑇𝑡 ↔ ¬ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉)) |
60 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉) → (𝑡𝑇u ↔
〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉)) |
61 | 60 | 3adant3 923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (𝑡𝑇u ↔
〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉)) |
62 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (u𝑇v ↔
〈𝑐, 𝑑〉𝑇〈𝑒, f〉)) |
63 | 62 | 3adant1 921 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (u𝑇v ↔
〈𝑐, 𝑑〉𝑇〈𝑒, f〉)) |
64 | 61, 63 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → ((𝑡𝑇u ∧ u𝑇v) ↔ (〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧
〈𝑐, 𝑑〉𝑇〈𝑒, f〉))) |
65 | | breq12 3760 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
v = 〈𝑒, f〉) → (𝑡𝑇v ↔
〈𝑎, 𝑏〉𝑇〈𝑒, f〉)) |
66 | 65 | 3adant2 922 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (𝑡𝑇v ↔
〈𝑎, 𝑏〉𝑇〈𝑒, f〉)) |
67 | 64, 66 | imbi12d 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)
↔ ((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧
〈𝑐, 𝑑〉𝑇〈𝑒, f〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, f〉))) |
68 | 59, 67 | anbi12d 442 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))
↔ (¬ 〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ∧
((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧
〈𝑐, 𝑑〉𝑇〈𝑒, f〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, f〉)))) |
69 | | poxp.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑇 = {〈x, y〉
∣ ((x ∈ (A ×
B) ∧
y ∈
(A × B)) ∧
((1st ‘x)𝑅(1st ‘y) ∨
((1st ‘x) =
(1st ‘y) ∧ (2nd ‘x)𝑆(2nd ‘y))))} |
70 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ↔ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏
∈ B))
∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
71 | 70 | notbii 593 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ↔ ¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏
∈ B))
∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))) |
72 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ↔ (((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑
∈ B))
∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)))) |
73 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑐, 𝑑〉𝑇〈𝑒, f〉
↔ (((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) |
74 | 72, 73 | anbi12i 433 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧
〈𝑐, 𝑑〉𝑇〈𝑒, f〉) ↔ ((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑
∈ B))
∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧
(((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))) |
75 | 69 | xporderlem 5793 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(〈𝑎, 𝑏〉𝑇〈𝑒, f〉
↔ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))) |
76 | 74, 75 | imbi12i 228 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧
〈𝑐, 𝑑〉𝑇〈𝑒, f〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, f〉) ↔ (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑
∈ B))
∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧
(((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
→ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))) |
77 | 71, 76 | anbi12i 433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
〈𝑎, 𝑏〉𝑇〈𝑎, 𝑏〉 ∧
((〈𝑎, 𝑏〉𝑇〈𝑐, 𝑑〉 ∧
〈𝑐, 𝑑〉𝑇〈𝑒, f〉) → 〈𝑎, 𝑏〉𝑇〈𝑒, f〉)) ↔ (¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏
∈ B))
∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧
(((((𝑎 ∈ A ∧ 𝑐
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧
(((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
→ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))) |
78 | 68, 77 | syl6bb 185 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))
↔ (¬ (((𝑎 ∈ A ∧ 𝑎
∈ A)
∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧
(((((𝑎 ∈ A ∧ 𝑐
∈ A)
∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧
(((𝑐 ∈ A ∧ 𝑒
∈ A)
∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
→ (((𝑎 ∈ A ∧ 𝑒
∈ A)
∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))))) |
79 | 55, 78 | syl5ibr 145 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (((𝑅 Po A
∧ 𝑆 Po B)
∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑
∈ B)
∧ (𝑒 ∈ A ∧ f ∈ B))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))) |
80 | 79 | expcomd 1327 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) → (((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑
∈ B)
∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑅 Po A
∧ 𝑆 Po B)
→ (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))) |
81 | 80 | imp 115 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑡 = 〈𝑎, 𝑏〉 ∧
u = 〈𝑐, 𝑑〉 ∧
v = 〈𝑒, f〉) ∧ ((𝑎 ∈ A ∧ 𝑏
∈ B)
∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) →
((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))) |
82 | 4, 81 | sylbi 114 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
∧ (u =
〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
∧ (v =
〈𝑒, f〉 ∧ (𝑒 ∈ A ∧ f ∈ B))) →
((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))) |
83 | 82 | 3exp 1102 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
→ ((u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
→ ((v = 〈𝑒, f〉
∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑅 Po A
∧ 𝑆 Po B)
→ (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))) |
84 | 83 | com3l 75 |
. . . . . . . . . . . . . 14
⊢
((u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
→ ((v = 〈𝑒, f〉
∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
→ ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))) |
85 | 84 | exlimivv 1773 |
. . . . . . . . . . . . 13
⊢ (∃𝑐∃𝑑(u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
→ ((v = 〈𝑒, f〉
∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
→ ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))) |
86 | 85 | com3l 75 |
. . . . . . . . . . . 12
⊢
((v = 〈𝑒, f〉
∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
→ (∃𝑐∃𝑑(u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
→ ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))) |
87 | 86 | exlimivv 1773 |
. . . . . . . . . . 11
⊢ (∃𝑒∃f(v =
〈𝑒, f〉 ∧ (𝑒 ∈ A ∧ f ∈ B)) →
((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
→ (∃𝑐∃𝑑(u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
→ ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))) |
88 | 87 | com3l 75 |
. . . . . . . . . 10
⊢ ((𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
→ (∃𝑐∃𝑑(u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
→ (∃𝑒∃f(v =
〈𝑒, f〉 ∧ (𝑒 ∈ A ∧ f ∈ B)) →
((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))) |
89 | 88 | exlimivv 1773 |
. . . . . . . . 9
⊢ (∃𝑎∃𝑏(𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
→ (∃𝑐∃𝑑(u = 〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
→ (∃𝑒∃f(v =
〈𝑒, f〉 ∧ (𝑒 ∈ A ∧ f ∈ B)) →
((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))) |
90 | 89 | 3imp 1097 |
. . . . . . . 8
⊢ ((∃𝑎∃𝑏(𝑡 = 〈𝑎, 𝑏〉 ∧
(𝑎 ∈ A ∧ 𝑏
∈ B))
∧ ∃𝑐∃𝑑(u =
〈𝑐, 𝑑〉 ∧
(𝑐 ∈ A ∧ 𝑑
∈ B))
∧ ∃𝑒∃f(v = 〈𝑒, f〉
∧ (𝑒 ∈ A ∧ f ∈ B))) → ((𝑅 Po A
∧ 𝑆 Po B)
→ (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))) |
91 | 1, 2, 3, 90 | syl3anb 1177 |
. . . . . . 7
⊢ ((𝑡 ∈ (A ×
B) ∧
u ∈
(A × B) ∧ v ∈ (A × B))
→ ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))) |
92 | 91 | 3expia 1105 |
. . . . . 6
⊢ ((𝑡 ∈ (A ×
B) ∧
u ∈
(A × B)) → (v
∈ (A
× B) → ((𝑅 Po A
∧ 𝑆 Po B)
→ (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))) |
93 | 92 | com3r 73 |
. . . . 5
⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ((𝑡 ∈
(A × B) ∧ u ∈ (A × B))
→ (v ∈ (A ×
B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))) |
94 | 93 | imp 115 |
. . . 4
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑡 ∈ (A ×
B) ∧
u ∈
(A × B))) → (v
∈ (A
× B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))) |
95 | 94 | ralrimiv 2385 |
. . 3
⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑡 ∈ (A ×
B) ∧
u ∈
(A × B))) → ∀v ∈ (A ×
B)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))) |
96 | 95 | ralrimivva 2395 |
. 2
⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ∀𝑡 ∈ (A ×
B)∀u ∈ (A ×
B)∀v ∈ (A ×
B)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))) |
97 | | df-po 4024 |
. 2
⊢ (𝑇 Po (A × B)
↔ ∀𝑡 ∈
(A × B)∀u ∈ (A × B)∀v ∈ (A × B)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))) |
98 | 96, 97 | sylibr 137 |
1
⊢ ((𝑅 Po A ∧ 𝑆 Po B) → 𝑇 Po (A
× B)) |