Proof of Theorem xpord3inddlem
Step | Hyp | Ref
| Expression |
1 | | xpord3.1 |
. . . 4
⊢ 𝑈 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st
‘(1st ‘𝑥))𝑅(1st ‘(1st
‘𝑦)) ∨
(1st ‘(1st ‘𝑥)) = (1st ‘(1st
‘𝑦))) ∧
((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st
‘𝑦)) ∨
(2nd ‘(1st ‘𝑥)) = (2nd ‘(1st
‘𝑦))) ∧
((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))} |
2 | | xpord3inddlem.1 |
. . . 4
⊢ (𝜅 → 𝑅 Fr 𝐴) |
3 | | xpord3inddlem.4 |
. . . 4
⊢ (𝜅 → 𝑆 Fr 𝐵) |
4 | | xpord3inddlem.7 |
. . . 4
⊢ (𝜅 → 𝑇 Fr 𝐶) |
5 | 1, 2, 3, 4 | frxp3 8132 |
. . 3
⊢ (𝜅 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶)) |
6 | | xpord3inddlem.2 |
. . . 4
⊢ (𝜅 → 𝑅 Po 𝐴) |
7 | | xpord3inddlem.5 |
. . . 4
⊢ (𝜅 → 𝑆 Po 𝐵) |
8 | | xpord3inddlem.8 |
. . . 4
⊢ (𝜅 → 𝑇 Po 𝐶) |
9 | 1, 6, 7, 8 | poxp3 8131 |
. . 3
⊢ (𝜅 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶)) |
10 | | xpord3inddlem.3 |
. . . 4
⊢ (𝜅 → 𝑅 Se 𝐴) |
11 | | xpord3inddlem.6 |
. . . 4
⊢ (𝜅 → 𝑆 Se 𝐵) |
12 | | xpord3inddlem.9 |
. . . 4
⊢ (𝜅 → 𝑇 Se 𝐶) |
13 | 1, 10, 11, 12 | sexp3 8134 |
. . 3
⊢ (𝜅 → 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) |
14 | | xpord3inddlem.x |
. . 3
⊢ (𝜅 → 𝑋 ∈ 𝐴) |
15 | | xpord3inddlem.y |
. . 3
⊢ (𝜅 → 𝑌 ∈ 𝐵) |
16 | | xpord3inddlem.z |
. . 3
⊢ (𝜅 → 𝑍 ∈ 𝐶) |
17 | | bi2.04 389 |
. . . . . . 7
⊢
((〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → (𝜅 → 𝜃)) ↔ (𝜅 → (〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
18 | 17 | 3albii 1824 |
. . . . . 6
⊢
(∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → (𝜅 → 𝜃)) ↔ ∀𝑑∀𝑒∀𝑓(𝜅 → (〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
19 | | 19.21v 1943 |
. . . . . . . 8
⊢
(∀𝑓(𝜅 → (〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) ↔ (𝜅 → ∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
20 | 19 | 2albii 1823 |
. . . . . . 7
⊢
(∀𝑑∀𝑒∀𝑓(𝜅 → (〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) ↔ ∀𝑑∀𝑒(𝜅 → ∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
21 | | 19.21v 1943 |
. . . . . . . . 9
⊢
(∀𝑒(𝜅 → ∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) ↔ (𝜅 → ∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
22 | 21 | albii 1822 |
. . . . . . . 8
⊢
(∀𝑑∀𝑒(𝜅 → ∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) ↔ ∀𝑑(𝜅 → ∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
23 | | 19.21v 1943 |
. . . . . . . 8
⊢
(∀𝑑(𝜅 → ∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
24 | 22, 23 | bitri 275 |
. . . . . . 7
⊢
(∀𝑑∀𝑒(𝜅 → ∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
25 | 20, 24 | bitri 275 |
. . . . . 6
⊢
(∀𝑑∀𝑒∀𝑓(𝜅 → (〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
26 | 18, 25 | bitri 275 |
. . . . 5
⊢
(∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → (𝜅 → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃))) |
27 | 1 | xpord3pred 8133 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) |
28 | 27 | adantl 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉})) |
29 | 28 | eleq2d 2820 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) ↔ 〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}))) |
30 | 29 | imbi1d 342 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) ↔ (〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) → 𝜃))) |
31 | | eldifsn 4789 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ↔ (〈𝑑, 𝑒, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ 〈𝑑, 𝑒, 𝑓〉 ≠ 〈𝑎, 𝑏, 𝑐〉)) |
32 | | otelxp 5718 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}))) |
33 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑑 ∈ V |
34 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑒 ∈ V |
35 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
36 | 33, 34, 35 | otthne 5485 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑑, 𝑒, 𝑓〉 ≠ 〈𝑎, 𝑏, 𝑐〉 ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
37 | 32, 36 | anbi12i 628 |
. . . . . . . . . . . . . . 15
⊢
((〈𝑑, 𝑒, 𝑓〉 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ 〈𝑑, 𝑒, 𝑓〉 ≠ 〈𝑎, 𝑏, 𝑐〉) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) |
38 | 31, 37 | bitri 275 |
. . . . . . . . . . . . . 14
⊢
(〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) |
39 | 38 | imbi1i 350 |
. . . . . . . . . . . . 13
⊢
((〈𝑑, 𝑒, 𝑓〉 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {〈𝑎, 𝑏, 𝑐〉}) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃)) |
40 | 30, 39 | bitrdi 287 |
. . . . . . . . . . . 12
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃))) |
41 | | impexp 452 |
. . . . . . . . . . . 12
⊢ ((((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
42 | 40, 41 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))) |
43 | 42 | albidv 1924 |
. . . . . . . . . 10
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) ↔ ∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))) |
44 | 43 | 2albidv 1927 |
. . . . . . . . 9
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))) |
45 | | r3al 3197 |
. . . . . . . . . 10
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
46 | 45 | bicomi 223 |
. . . . . . . . 9
⊢
(∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
47 | 44, 46 | bitrdi 287 |
. . . . . . . 8
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
48 | | ssun1 4171 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) |
49 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑓 ∈
(Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
51 | 50 | ralimi 3084 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
52 | | ssun1 4171 |
. . . . . . . . . . . . . . . . . . 19
⊢
Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) |
53 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . . 19
⊢
(Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
55 | 51, 54 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
56 | 55 | ralimi 3084 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
57 | | ssun1 4171 |
. . . . . . . . . . . . . . . . 17
⊢
Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) |
58 | | ssralv 4049 |
. . . . . . . . . . . . . . . . 17
⊢
(Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
60 | 56, 59 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
61 | 60 | adantl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
62 | | predpoirr 6331 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)) |
63 | 8, 62 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜅 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)) |
64 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑐 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))) |
65 | 64 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑐 → (¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))) |
66 | 63, 65 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜅 → (𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐))) |
67 | 66 | necon2ad 2956 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜅 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → 𝑓 ≠ 𝑐)) |
68 | 67 | imp 408 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → 𝑓 ≠ 𝑐) |
69 | 68 | 3mix3d 1339 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
70 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃)) |
72 | 71 | ralimdva 3168 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)) |
73 | 72 | ralimdv 3170 |
. . . . . . . . . . . . . . . 16
⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)) |
74 | 73 | ralimdv 3170 |
. . . . . . . . . . . . . . 15
⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)) |
75 | 74 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)) |
76 | 61, 75 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃) |
77 | | ssun2 4172 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) |
78 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
79 | 77, 78 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑓 ∈
(Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
80 | 79 | ralimi 3084 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
81 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
82 | 52, 81 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
83 | 80, 82 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
84 | 83 | ralimi 3084 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
85 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . 18
⊢
(Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
86 | 57, 85 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
87 | 84, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
88 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑐 ∈ V |
89 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑐 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎)) |
90 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑐 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏)) |
91 | | neeq1 3004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑐 → (𝑓 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐)) |
92 | 89, 90, 91 | 3orbi123d 1436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑐 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))) |
93 | | xpord3inddlem.12 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) |
94 | 93 | equcoms 2024 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑐 → (𝜒 ↔ 𝜃)) |
95 | 94 | bicomd 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑐 → (𝜃 ↔ 𝜒)) |
96 | 92, 95 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = 𝑐 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))) |
97 | 88, 96 | ralsn 4684 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑓 ∈
{𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)) |
98 | 97 | 2ralbii 3129 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)) |
99 | 87, 98 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)) |
100 | 99 | adantl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)) |
101 | | predpoirr 6331 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)) |
102 | 7, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜅 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)) |
103 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑒 = 𝑏 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))) |
104 | 103 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑒 = 𝑏 → (¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))) |
105 | 102, 104 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜅 → (𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏))) |
106 | 105 | necon2ad 2956 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜅 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑒 ≠ 𝑏)) |
107 | 106 | imp 408 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → 𝑒 ≠ 𝑏) |
108 | 107 | 3mix2d 1338 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)) |
109 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒)) |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒)) |
111 | 110 | ralimdva 3168 |
. . . . . . . . . . . . . . . 16
⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)) |
112 | 111 | ralimdv 3170 |
. . . . . . . . . . . . . . 15
⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)) |
113 | 112 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)) |
114 | 100, 113 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒) |
115 | | ssun2 4172 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) |
116 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
117 | 115, 116 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
118 | 51, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
119 | 118 | ralimi 3084 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
120 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . 18
⊢
(Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
121 | 57, 120 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
122 | 119, 121 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
123 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑏 ∈ V |
124 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑏 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎)) |
125 | | neeq1 3004 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑏 → (𝑒 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏)) |
126 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑏 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐)) |
127 | 124, 125,
126 | 3orbi123d 1436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) |
128 | | xpord3inddlem.15 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) |
129 | 128 | equcoms 2024 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑏 → (𝜁 ↔ 𝜃)) |
130 | 129 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑏 → (𝜃 ↔ 𝜁)) |
131 | 127, 130 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))) |
132 | 131 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))) |
133 | 123, 132 | ralsn 4684 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑒 ∈
{𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)) |
134 | 133 | ralbii 3094 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)) |
135 | 122, 134 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)) |
136 | 135 | adantl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)) |
137 | 68 | 3mix3d 1339 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
138 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁)) |
139 | 137, 138 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁)) |
140 | 139 | ralimdva 3168 |
. . . . . . . . . . . . . . . 16
⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)) |
141 | 140 | ralimdv 3170 |
. . . . . . . . . . . . . . 15
⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)) |
142 | 141 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)) |
143 | 136, 142 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) |
144 | 76, 114, 143 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)) |
145 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
146 | 115, 145 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
147 | 80, 146 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑒 ∈
(Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
148 | 147 | ralimi 3084 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
149 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . 18
⊢
(Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
150 | 57, 149 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
151 | 148, 150 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
152 | 97 | ralbii 3094 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑒 ∈
{𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)) |
153 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑏 → (𝑐 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐)) |
154 | 124, 125,
153 | 3orbi123d 1436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))) |
155 | | xpord3inddlem.11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) |
156 | 155 | equcoms 2024 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑒 = 𝑏 → (𝜓 ↔ 𝜒)) |
157 | 156 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑏 → (𝜒 ↔ 𝜓)) |
158 | 154, 157 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))) |
159 | 123, 158 | ralsn 4684 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑒 ∈
{𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)) |
160 | 152, 159 | bitri 275 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑒 ∈
{𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)) |
161 | 160 | ralbii 3094 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)) |
162 | 151, 161 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)) |
163 | 162 | adantl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)) |
164 | | predpoirr 6331 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)) |
165 | 6, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜅 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)) |
166 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 = 𝑎 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))) |
167 | 166 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 = 𝑎 → (¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))) |
168 | 165, 167 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜅 → (𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎))) |
169 | 168 | necon2ad 2956 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜅 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑑 ≠ 𝑎)) |
170 | 169 | imp 408 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → 𝑑 ≠ 𝑎) |
171 | 170 | 3mix1d 1337 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)) |
172 | | pm2.27 42 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓)) |
173 | 171, 172 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓)) |
174 | 173 | ralimdva 3168 |
. . . . . . . . . . . . . . 15
⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)) |
175 | 174 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)) |
176 | 163, 175 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓) |
177 | | ssun2 4172 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) |
178 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
179 | 177, 178 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
180 | 56, 179 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
181 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑎 ∈ V |
182 | | neeq1 3004 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → (𝑑 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎)) |
183 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏)) |
184 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐)) |
185 | 182, 183,
184 | 3orbi123d 1436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = 𝑎 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) |
186 | | xpord3inddlem.13 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) |
187 | 186 | equcoms 2024 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = 𝑎 → (𝜏 ↔ 𝜃)) |
188 | 187 | bicomd 222 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = 𝑎 → (𝜃 ↔ 𝜏)) |
189 | 185, 188 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑎 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))) |
190 | 189 | 2ralbidv 3219 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))) |
191 | 181, 190 | ralsn 4684 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
{𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)) |
192 | 180, 191 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)) |
193 | 192 | adantl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)) |
194 | 68 | 3mix3d 1339 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
195 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏)) |
196 | 194, 195 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏)) |
197 | 196 | ralimdva 3168 |
. . . . . . . . . . . . . . . 16
⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)) |
198 | 197 | ralimdv 3170 |
. . . . . . . . . . . . . . 15
⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)) |
199 | 198 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)) |
200 | 193, 199 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏) |
201 | | ssralv 4049 |
. . . . . . . . . . . . . . . . . 18
⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
202 | 177, 201 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
203 | 84, 202 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
204 | 189 | 2ralbidv 3219 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))) |
205 | 181, 204 | ralsn 4684 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑑 ∈
{𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)) |
206 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = 𝑐 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎)) |
207 | 206, 90, 91 | 3orbi123d 1436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑐 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))) |
208 | | xpord3inddlem.16 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) |
209 | 208 | bicomd 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑐 = 𝑓 → (𝜏 ↔ 𝜎)) |
210 | 209 | equcoms 2024 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = 𝑐 → (𝜏 ↔ 𝜎)) |
211 | 207, 210 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = 𝑐 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))) |
212 | 88, 211 | ralsn 4684 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑓 ∈
{𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)) |
213 | 212 | ralbii 3094 |
. . . . . . . . . . . . . . . . 17
⊢
(∀𝑒 ∈
Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)) |
214 | 205, 213 | bitri 275 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
{𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)) |
215 | 203, 214 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)) |
216 | 215 | adantl 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)) |
217 | 107 | 3mix2d 1338 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)) |
218 | | pm2.27 42 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎)) |
219 | 217, 218 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎)) |
220 | 219 | ralimdva 3168 |
. . . . . . . . . . . . . . 15
⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)) |
221 | 220 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)) |
222 | 216, 221 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) |
223 | 176, 200,
222 | 3jca 1129 |
. . . . . . . . . . . 12
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)) |
224 | | ssralv 4049 |
. . . . . . . . . . . . . . . . 17
⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))) |
225 | 177, 224 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
226 | 119, 225 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) |
227 | 189 | 2ralbidv 3219 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))) |
228 | 181, 227 | ralsn 4684 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑑 ∈
{𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)) |
229 | | biidd 262 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑏 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎)) |
230 | 229, 125,
126 | 3orbi123d 1436 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑏 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) |
231 | | equcomi 2021 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑒 = 𝑏 → 𝑏 = 𝑒) |
232 | | xpord3inddlem.14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) |
233 | | bicom1 220 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜂 ↔ 𝜏) → (𝜏 ↔ 𝜂)) |
234 | 231, 232,
233 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑒 = 𝑏 → (𝜏 ↔ 𝜂)) |
235 | 230, 234 | imbi12d 345 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑒 = 𝑏 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))) |
236 | 235 | ralbidv 3178 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))) |
237 | 123, 236 | ralsn 4684 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑒 ∈
{𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)) |
238 | 228, 237 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑑 ∈
{𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)) |
239 | 226, 238 | sylib 217 |
. . . . . . . . . . . . . 14
⊢
(∀𝑑 ∈
(Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)) |
240 | 239 | adantl 483 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)) |
241 | 68 | 3mix3d 1339 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) |
242 | | pm2.27 42 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂)) |
243 | 241, 242 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂)) |
244 | 243 | ralimdva 3168 |
. . . . . . . . . . . . . 14
⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)) |
245 | 244 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)) |
246 | 240, 245 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) |
247 | 144, 223,
246 | 3jca 1129 |
. . . . . . . . . . 11
⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)) |
248 | 247 | ex 414 |
. . . . . . . . . 10
⊢ (𝜅 → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))) |
249 | 248 | adantr 482 |
. . . . . . . . 9
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))) |
250 | | xpord3inddlem.i |
. . . . . . . . 9
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑)) |
251 | 249, 250 | syld 47 |
. . . . . . . 8
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜑)) |
252 | 47, 251 | sylbid 239 |
. . . . . . 7
⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) → 𝜑)) |
253 | 252 | expcom 415 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝜅 → (∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃) → 𝜑))) |
254 | 253 | a2d 29 |
. . . . 5
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝜅 → ∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → 𝜃)) → (𝜅 → 𝜑))) |
255 | 26, 254 | biimtrid 241 |
. . . 4
⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(〈𝑑, 𝑒, 𝑓〉 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), 〈𝑎, 𝑏, 𝑐〉) → (𝜅 → 𝜃)) → (𝜅 → 𝜑))) |
256 | | xpord3inddlem.10 |
. . . . 5
⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) |
257 | 256 | imbi2d 341 |
. . . 4
⊢ (𝑎 = 𝑑 → ((𝜅 → 𝜑) ↔ (𝜅 → 𝜓))) |
258 | 155 | imbi2d 341 |
. . . 4
⊢ (𝑏 = 𝑒 → ((𝜅 → 𝜓) ↔ (𝜅 → 𝜒))) |
259 | 93 | imbi2d 341 |
. . . 4
⊢ (𝑐 = 𝑓 → ((𝜅 → 𝜒) ↔ (𝜅 → 𝜃))) |
260 | | xpord3inddlem.17 |
. . . . 5
⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) |
261 | 260 | imbi2d 341 |
. . . 4
⊢ (𝑎 = 𝑋 → ((𝜅 → 𝜑) ↔ (𝜅 → 𝜌))) |
262 | | xpord3inddlem.18 |
. . . . 5
⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) |
263 | 262 | imbi2d 341 |
. . . 4
⊢ (𝑏 = 𝑌 → ((𝜅 → 𝜌) ↔ (𝜅 → 𝜇))) |
264 | | xpord3inddlem.19 |
. . . . 5
⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) |
265 | 264 | imbi2d 341 |
. . . 4
⊢ (𝑐 = 𝑍 → ((𝜅 → 𝜇) ↔ (𝜅 → 𝜆))) |
266 | 255, 257,
258, 259, 261, 263, 265 | frpoins3xp3g 8122 |
. . 3
⊢ (((𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → (𝜅 → 𝜆)) |
267 | 5, 9, 13, 14, 15, 16, 266 | syl33anc 1386 |
. 2
⊢ (𝜅 → (𝜅 → 𝜆)) |
268 | 267 | pm2.43i 52 |
1
⊢ (𝜅 → 𝜆) |