Step | Hyp | Ref
| Expression |
1 | | elxpxp 33249 |
. . . 4
⊢ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉) |
2 | | neirr 2943 |
. . . . . . . . . . 11
⊢ ¬
𝑑 ≠ 𝑑 |
3 | | neirr 2943 |
. . . . . . . . . . 11
⊢ ¬
𝑒 ≠ 𝑒 |
4 | | neirr 2943 |
. . . . . . . . . . 11
⊢ ¬
𝑓 ≠ 𝑓 |
5 | 2, 3, 4 | 3pm3.2ni 33221 |
. . . . . . . . . 10
⊢ ¬
(𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓) |
6 | 5 | intnan 490 |
. . . . . . . . 9
⊢ ¬
(((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)) |
7 | | simp3 1139 |
. . . . . . . . 9
⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))) → (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))) |
8 | 6, 7 | mto 200 |
. . . . . . . 8
⊢ ¬
((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))) |
9 | | breq12 5032 |
. . . . . . . . . 10
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉) → (𝑎𝑈𝑎 ↔ 〈〈𝑑, 𝑒〉, 𝑓〉𝑈〈〈𝑑, 𝑒〉, 𝑓〉)) |
10 | 9 | anidms 570 |
. . . . . . . . 9
⊢ (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑎𝑈𝑎 ↔ 〈〈𝑑, 𝑒〉, 𝑓〉𝑈〈〈𝑑, 𝑒〉, 𝑓〉)) |
11 | | xpord3.1 |
. . . . . . . . . 10
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
12 | 11 | xpord3lem 33398 |
. . . . . . . . 9
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉𝑈〈〈𝑑, 𝑒〉, 𝑓〉 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)))) |
13 | 10, 12 | bitrdi 290 |
. . . . . . . 8
⊢ (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 → (𝑎𝑈𝑎 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))))) |
14 | 8, 13 | mtbiri 330 |
. . . . . . 7
⊢ (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ¬ 𝑎𝑈𝑎) |
15 | 14 | rexlimivw 3191 |
. . . . . 6
⊢
(∃𝑓 ∈
𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ¬ 𝑎𝑈𝑎) |
16 | 15 | a1i 11 |
. . . . 5
⊢ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵) → (∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ¬ 𝑎𝑈𝑎)) |
17 | 16 | rexlimivv 3201 |
. . . 4
⊢
(∃𝑑 ∈
𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 → ¬ 𝑎𝑈𝑎) |
18 | 1, 17 | sylbi 220 |
. . 3
⊢ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) → ¬ 𝑎𝑈𝑎) |
19 | 18 | adantl 485 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ((𝐴 × 𝐵) × 𝐶)) → ¬ 𝑎𝑈𝑎) |
20 | | elxpxp 33249 |
. . . . . 6
⊢ (𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉) |
21 | | elxpxp 33249 |
. . . . . 6
⊢ (𝑐 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) |
22 | 1, 20, 21 | 3anbi123i 1156 |
. . . . 5
⊢ ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
23 | | 3reeanv 3270 |
. . . . . . . . . . 11
⊢
(∃𝑓 ∈
𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ (∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
24 | 23 | rexbii 3160 |
. . . . . . . . . 10
⊢
(∃𝑘 ∈
𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
25 | 24 | 2rexbii 3161 |
. . . . . . . . 9
⊢
(∃𝑒 ∈
𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
26 | | 3reeanv 3270 |
. . . . . . . . 9
⊢
(∃𝑒 ∈
𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
27 | 25, 26 | bitri 278 |
. . . . . . . 8
⊢
(∃𝑒 ∈
𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
28 | 27 | rexbii 3160 |
. . . . . . 7
⊢
(∃𝑗 ∈
𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
29 | 28 | 2rexbii 3161 |
. . . . . 6
⊢
(∃𝑑 ∈
𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
30 | | 3reeanv 3270 |
. . . . . 6
⊢
(∃𝑑 ∈
𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
31 | 29, 30 | bitri 278 |
. . . . 5
⊢
(∃𝑑 ∈
𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
32 | 22, 31 | bitr4i 281 |
. . . 4
⊢ ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉)) |
33 | | simprl1 1219 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) |
34 | | simprr2 1223 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶)) |
35 | | poxp3.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑅 Po 𝐴) |
36 | 35 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑅 Po 𝐴) |
37 | | simpl11 1249 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑑 ∈ 𝐴) |
38 | 37 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑑 ∈ 𝐴) |
39 | | simpr11 1258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑔 ∈ 𝐴) |
40 | 39 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑔 ∈ 𝐴) |
41 | | simpr21 1261 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑗 ∈ 𝐴) |
42 | 41 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑗 ∈ 𝐴) |
43 | | potr 5450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑅 Po 𝐴 ∧ (𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴)) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → 𝑑𝑅𝑗)) |
44 | 36, 38, 40, 42, 43 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → 𝑑𝑅𝑗)) |
45 | | orc 866 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)) |
46 | 44, 45 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))) |
47 | 46 | expd 419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))) |
48 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑗 ↔ 𝑔𝑅𝑗)) |
49 | 48, 45 | syl6bir 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))) |
50 | 49 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))) |
51 | | simp3l1 1279 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔)) |
52 | 51 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔)) |
53 | 47, 50, 52 | mpjaod 859 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))) |
54 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑗 → (𝑑𝑅𝑔 ↔ 𝑑𝑅𝑗)) |
55 | | equequ2 2037 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑑 = 𝑗)) |
56 | 54, 55 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑔 = 𝑗 → ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ↔ (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))) |
57 | 52, 56 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔 = 𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))) |
58 | | simp3l1 1279 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗)) |
59 | 58 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗)) |
60 | 53, 57, 59 | mpjaod 859 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)) |
61 | | poxp3.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑆 Po 𝐵) |
62 | 61 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑆 Po 𝐵) |
63 | | simpl12 1250 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑒 ∈ 𝐵) |
64 | 63 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑒 ∈ 𝐵) |
65 | | simpr12 1259 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ℎ ∈ 𝐵) |
66 | 65 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ℎ ∈ 𝐵) |
67 | | simpr22 1262 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑘 ∈ 𝐵) |
68 | 67 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑘 ∈ 𝐵) |
69 | | potr 5450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑆 Po 𝐵 ∧ (𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ∧ 𝑘 ∈ 𝐵)) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → 𝑒𝑆𝑘)) |
70 | 62, 64, 66, 68, 69 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → 𝑒𝑆𝑘)) |
71 | | orc 866 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)) |
72 | 70, 71 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))) |
73 | 72 | expd 419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))) |
74 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = ℎ → (𝑒𝑆𝑘 ↔ ℎ𝑆𝑘)) |
75 | 74, 71 | syl6bir 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))) |
76 | 75 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))) |
77 | | simp3l2 1280 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ)) |
78 | 77 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ)) |
79 | 73, 76, 78 | mpjaod 859 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))) |
80 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑘 → (𝑒𝑆ℎ ↔ 𝑒𝑆𝑘)) |
81 | | equequ2 2037 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑘 → (𝑒 = ℎ ↔ 𝑒 = 𝑘)) |
82 | 80, 81 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑘 → ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ↔ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))) |
83 | 78, 82 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ = 𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))) |
84 | | simp3l2 1280 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘)) |
85 | 84 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘)) |
86 | 79, 83, 85 | mpjaod 859 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)) |
87 | | poxp3.3 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑇 Po 𝐶) |
88 | 87 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑇 Po 𝐶) |
89 | | simpl13 1251 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑓 ∈ 𝐶) |
90 | 89 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑓 ∈ 𝐶) |
91 | | simpr13 1260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑖 ∈ 𝐶) |
92 | 91 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑖 ∈ 𝐶) |
93 | | simpr23 1263 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑙 ∈ 𝐶) |
94 | 93 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑙 ∈ 𝐶) |
95 | | potr 5450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑇 Po 𝐶 ∧ (𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶 ∧ 𝑙 ∈ 𝐶)) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → 𝑓𝑇𝑙)) |
96 | 88, 90, 92, 94, 95 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → 𝑓𝑇𝑙)) |
97 | | orc 866 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) |
98 | 96, 97 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))) |
99 | 98 | expd 419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))) |
100 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑙 ↔ 𝑖𝑇𝑙)) |
101 | 100, 97 | syl6bir 257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))) |
102 | 101 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))) |
103 | | simp3l3 1281 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) |
104 | 103 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) |
105 | 99, 102, 104 | mpjaod 859 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))) |
106 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑙 → (𝑓𝑇𝑖 ↔ 𝑓𝑇𝑙)) |
107 | | equequ2 2037 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑙 → (𝑓 = 𝑖 ↔ 𝑓 = 𝑙)) |
108 | 106, 107 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑙 → ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ↔ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))) |
109 | 104, 108 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖 = 𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))) |
110 | | simp3l3 1281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) |
111 | 110 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) |
112 | 105, 109,
111 | mpjaod 859 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) |
113 | 60, 86, 112 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))) |
114 | | simpr3r 1236 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)) |
115 | 114 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)) |
116 | | df-ne 2935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑔 ≠ 𝑗 ↔ ¬ 𝑔 = 𝑗) |
117 | | df-ne 2935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ ≠ 𝑘 ↔ ¬ ℎ = 𝑘) |
118 | | df-ne 2935 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ≠ 𝑙 ↔ ¬ 𝑖 = 𝑙) |
119 | 116, 117,
118 | 3orbi123i 1157 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ ℎ = 𝑘 ∨ ¬ 𝑖 = 𝑙)) |
120 | | 3ianor 1108 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (¬
(𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ ℎ = 𝑘 ∨ ¬ 𝑖 = 𝑙)) |
121 | 119, 120 | bitr4i 281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙) ↔ ¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙)) |
122 | 115, 121 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙)) |
123 | | df-ne 2935 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 ≠ 𝑗 ↔ ¬ 𝑑 = 𝑗) |
124 | | df-ne 2935 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 ≠ 𝑘 ↔ ¬ 𝑒 = 𝑘) |
125 | | df-ne 2935 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ≠ 𝑙 ↔ ¬ 𝑓 = 𝑙) |
126 | 123, 124,
125 | 3orbi123i 1157 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙)) |
127 | | 3ianor 1108 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
(𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙)) |
128 | 126, 127 | bitr4i 281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) ↔ ¬ (𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙)) |
129 | 128 | con2bii 361 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) ↔ ¬ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)) |
130 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑑 = 𝑗 → (𝑑𝑅𝑔 ↔ 𝑗𝑅𝑔)) |
131 | | equequ1 2036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑑 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑗 = 𝑔)) |
132 | | equcom 2029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑗 = 𝑔 ↔ 𝑔 = 𝑗) |
133 | 131, 132 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑑 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑔 = 𝑗)) |
134 | 130, 133 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑑 = 𝑗 → ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ↔ (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗))) |
135 | 52, 134 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑗 → (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗))) |
136 | 135 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗)) |
137 | 59 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗)) |
138 | | ordir 1006 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗) ∨ 𝑔 = 𝑗) ↔ ((𝑗𝑅𝑔 ∨ 𝑔 = 𝑗) ∧ (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗))) |
139 | 136, 137,
138 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → ((𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗) ∨ 𝑔 = 𝑗)) |
140 | | po2nr 5451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑅 Po 𝐴 ∧ (𝑗 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗)) |
141 | 36, 42, 40, 140 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗)) |
142 | 141 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗)) |
143 | 139, 142 | orcnd 878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → 𝑔 = 𝑗) |
144 | 143 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑗 → 𝑔 = 𝑗)) |
145 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑒 = 𝑘 → (𝑒𝑆ℎ ↔ 𝑘𝑆ℎ)) |
146 | | equequ1 2036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑒 = 𝑘 → (𝑒 = ℎ ↔ 𝑘 = ℎ)) |
147 | | equcom 2029 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 = ℎ ↔ ℎ = 𝑘) |
148 | 146, 147 | bitrdi 290 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑒 = 𝑘 → (𝑒 = ℎ ↔ ℎ = 𝑘)) |
149 | 145, 148 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑒 = 𝑘 → ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ↔ (𝑘𝑆ℎ ∨ ℎ = 𝑘))) |
150 | 78, 149 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = 𝑘 → (𝑘𝑆ℎ ∨ ℎ = 𝑘))) |
151 | 150 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → (𝑘𝑆ℎ ∨ ℎ = 𝑘)) |
152 | 85 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘)) |
153 | | ordir 1006 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑘𝑆ℎ ∧ ℎ𝑆𝑘) ∨ ℎ = 𝑘) ↔ ((𝑘𝑆ℎ ∨ ℎ = 𝑘) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘))) |
154 | 151, 152,
153 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ((𝑘𝑆ℎ ∧ ℎ𝑆𝑘) ∨ ℎ = 𝑘)) |
155 | | po2nr 5451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑆 Po 𝐵 ∧ (𝑘 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘)) |
156 | 62, 68, 66, 155 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘)) |
157 | 156 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘)) |
158 | 154, 157 | orcnd 878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ℎ = 𝑘) |
159 | 158 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = 𝑘 → ℎ = 𝑘)) |
160 | | breq1 5030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑙 → (𝑓𝑇𝑖 ↔ 𝑙𝑇𝑖)) |
161 | | equequ1 2036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑙 → (𝑓 = 𝑖 ↔ 𝑙 = 𝑖)) |
162 | 160, 161 | orbi12d 918 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑙 → ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ↔ (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖))) |
163 | 104, 162 | syl5ibcom 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑙 → (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖))) |
164 | 163 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖)) |
165 | | equcom 2029 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑙 = 𝑖 ↔ 𝑖 = 𝑙) |
166 | 165 | orbi2i 912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙𝑇𝑖 ∨ 𝑙 = 𝑖) ↔ (𝑙𝑇𝑖 ∨ 𝑖 = 𝑙)) |
167 | 164, 166 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖 ∨ 𝑖 = 𝑙)) |
168 | 111 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) |
169 | | ordir 1006 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙) ∨ 𝑖 = 𝑙) ↔ ((𝑙𝑇𝑖 ∨ 𝑖 = 𝑙) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙))) |
170 | 167, 168,
169 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → ((𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙) ∨ 𝑖 = 𝑙)) |
171 | | po2nr 5451 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑇 Po 𝐶 ∧ (𝑙 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶)) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙)) |
172 | 88, 94, 92, 171 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙)) |
173 | 172 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙)) |
174 | 170, 173 | orcnd 878 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → 𝑖 = 𝑙) |
175 | 174 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑙 → 𝑖 = 𝑙)) |
176 | 144, 159,
175 | 3anim123d 1444 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) → (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙))) |
177 | 129, 176 | syl5bir 246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (¬ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) → (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙))) |
178 | 122, 177 | mt3d 150 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)) |
179 | 113, 178 | jca 515 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))) |
180 | 33, 34, 179 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))) |
181 | 180 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))) |
182 | | breq12 5032 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉) → (𝑎𝑈𝑏 ↔ 〈〈𝑑, 𝑒〉, 𝑓〉𝑈〈〈𝑔, ℎ〉, 𝑖〉)) |
183 | 182 | 3adant3 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑎𝑈𝑏 ↔ 〈〈𝑑, 𝑒〉, 𝑓〉𝑈〈〈𝑔, ℎ〉, 𝑖〉)) |
184 | 11 | xpord3lem 33398 |
. . . . . . . . . . . . . . . . 17
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉𝑈〈〈𝑔, ℎ〉, 𝑖〉 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) |
185 | 183, 184 | bitrdi 290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑎𝑈𝑏 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) |
186 | | breq12 5032 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑏𝑈𝑐 ↔ 〈〈𝑔, ℎ〉, 𝑖〉𝑈〈〈𝑗, 𝑘〉, 𝑙〉)) |
187 | 186 | 3adant1 1131 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑏𝑈𝑐 ↔ 〈〈𝑔, ℎ〉, 𝑖〉𝑈〈〈𝑗, 𝑘〉, 𝑙〉)) |
188 | 11 | xpord3lem 33398 |
. . . . . . . . . . . . . . . . 17
⊢
(〈〈𝑔,
ℎ〉, 𝑖〉𝑈〈〈𝑗, 𝑘〉, 𝑙〉 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) |
189 | 187, 188 | bitrdi 290 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑏𝑈𝑐 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) |
190 | 185, 189 | anbi12d 634 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))))) |
191 | | breq12 5032 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑎𝑈𝑐 ↔ 〈〈𝑑, 𝑒〉, 𝑓〉𝑈〈〈𝑗, 𝑘〉, 𝑙〉)) |
192 | 191 | 3adant2 1132 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑎𝑈𝑐 ↔ 〈〈𝑑, 𝑒〉, 𝑓〉𝑈〈〈𝑗, 𝑘〉, 𝑙〉)) |
193 | 11 | xpord3lem 33398 |
. . . . . . . . . . . . . . . 16
⊢
(〈〈𝑑,
𝑒〉, 𝑓〉𝑈〈〈𝑗, 𝑘〉, 𝑙〉 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))) |
194 | 192, 193 | bitrdi 290 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (𝑎𝑈𝑐 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))) |
195 | 190, 194 | imbi12d 348 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → (((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))))) |
196 | 181, 195 | syl5ibrcom 250 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
197 | 196 | rexlimdvw 3199 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
198 | 197 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶) → (∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))) |
199 | 198 | rexlimdvv 3202 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
200 | 199 | rexlimdvw 3199 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
201 | 200 | a1d 25 |
. . . . . . . 8
⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))) |
202 | 201 | rexlimdvv 3202 |
. . . . . . 7
⊢ (𝜑 → (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
203 | 202 | rexlimdvw 3199 |
. . . . . 6
⊢ (𝜑 → (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
204 | 203 | a1d 25 |
. . . . 5
⊢ (𝜑 → ((𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))) |
205 | 204 | rexlimdvv 3202 |
. . . 4
⊢ (𝜑 → (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = 〈〈𝑑, 𝑒〉, 𝑓〉 ∧ 𝑏 = 〈〈𝑔, ℎ〉, 𝑖〉 ∧ 𝑐 = 〈〈𝑗, 𝑘〉, 𝑙〉) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
206 | 32, 205 | syl5bi 245 |
. . 3
⊢ (𝜑 → ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))) |
207 | 206 | imp 410 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶))) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)) |
208 | 19, 207 | ispod 5446 |
1
⊢ (𝜑 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶)) |