MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpord3inddlem Structured version   Visualization version   GIF version

Theorem xpord3inddlem 8135
Description: Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025.)
Hypotheses
Ref Expression
xpord3.1 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
xpord3inddlem.x (𝜅𝑋𝐴)
xpord3inddlem.y (𝜅𝑌𝐵)
xpord3inddlem.z (𝜅𝑍𝐶)
xpord3inddlem.1 (𝜅𝑅 Fr 𝐴)
xpord3inddlem.2 (𝜅𝑅 Po 𝐴)
xpord3inddlem.3 (𝜅𝑅 Se 𝐴)
xpord3inddlem.4 (𝜅𝑆 Fr 𝐵)
xpord3inddlem.5 (𝜅𝑆 Po 𝐵)
xpord3inddlem.6 (𝜅𝑆 Se 𝐵)
xpord3inddlem.7 (𝜅𝑇 Fr 𝐶)
xpord3inddlem.8 (𝜅𝑇 Po 𝐶)
xpord3inddlem.9 (𝜅𝑇 Se 𝐶)
xpord3inddlem.10 (𝑎 = 𝑑 → (𝜑𝜓))
xpord3inddlem.11 (𝑏 = 𝑒 → (𝜓𝜒))
xpord3inddlem.12 (𝑐 = 𝑓 → (𝜒𝜃))
xpord3inddlem.13 (𝑎 = 𝑑 → (𝜏𝜃))
xpord3inddlem.14 (𝑏 = 𝑒 → (𝜂𝜏))
xpord3inddlem.15 (𝑏 = 𝑒 → (𝜁𝜃))
xpord3inddlem.16 (𝑐 = 𝑓 → (𝜎𝜏))
xpord3inddlem.17 (𝑎 = 𝑋 → (𝜑𝜌))
xpord3inddlem.18 (𝑏 = 𝑌 → (𝜌𝜇))
xpord3inddlem.19 (𝑐 = 𝑍 → (𝜇𝜆))
xpord3inddlem.i ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))
Assertion
Ref Expression
xpord3inddlem (𝜅𝜆)
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑥,𝐴,𝑦   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑥,𝐵,𝑦   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑥,𝐶,𝑦   𝑅,𝑑,𝑒,𝑓   𝑥,𝑅,𝑦   𝑆,𝑑,𝑒,𝑓   𝑥,𝑆,𝑦   𝑇,𝑑,𝑒,𝑓   𝑥,𝑇,𝑦   𝑈,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑋,𝑎,𝑏,𝑐   𝑌,𝑏,𝑐   𝑍,𝑐   𝜅,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝜓,𝑎   𝜌,𝑎   𝜃,𝑎   𝜒,𝑏,𝑓   𝜇,𝑏   𝜃,𝑏   𝜆,𝑐   𝜃,𝑐   𝜑,𝑑   𝜏,𝑑   𝜂,𝑒   𝜓,𝑒   𝜁,𝑒   𝜎,𝑓
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑐)   𝜓(𝑥,𝑦,𝑓,𝑏,𝑐,𝑑)   𝜒(𝑥,𝑦,𝑒,𝑎,𝑐,𝑑)   𝜃(𝑥,𝑦,𝑒,𝑓,𝑑)   𝜏(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑐)   𝜂(𝑥,𝑦,𝑓,𝑎,𝑏,𝑐,𝑑)   𝜁(𝑥,𝑦,𝑓,𝑎,𝑏,𝑐,𝑑)   𝜎(𝑥,𝑦,𝑒,𝑎,𝑏,𝑐,𝑑)   𝜌(𝑥,𝑦,𝑒,𝑓,𝑏,𝑐,𝑑)   𝜇(𝑥,𝑦,𝑒,𝑓,𝑎,𝑐,𝑑)   𝜆(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑑)   𝜅(𝑥,𝑦)   𝑅(𝑎,𝑏,𝑐)   𝑆(𝑎,𝑏,𝑐)   𝑇(𝑎,𝑏,𝑐)   𝑈(𝑥,𝑦)   𝑋(𝑥,𝑦,𝑒,𝑓,𝑑)   𝑌(𝑥,𝑦,𝑒,𝑓,𝑎,𝑑)   𝑍(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑑)

Proof of Theorem xpord3inddlem
StepHypRef 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 𝐶)
51, 2, 3, 4frxp3 8132 . . 3 (𝜅𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
6 xpord3inddlem.2 . . . 4 (𝜅𝑅 Po 𝐴)
7 xpord3inddlem.5 . . . 4 (𝜅𝑆 Po 𝐵)
8 xpord3inddlem.8 . . . 4 (𝜅𝑇 Po 𝐶)
91, 6, 7, 8poxp3 8131 . . 3 (𝜅𝑈 Po ((𝐴 × 𝐵) × 𝐶))
10 xpord3inddlem.3 . . . 4 (𝜅𝑅 Se 𝐴)
11 xpord3inddlem.6 . . . 4 (𝜅𝑆 Se 𝐵)
12 xpord3inddlem.9 . . . 4 (𝜅𝑇 Se 𝐶)
131, 10, 11, 12sexp3 8134 . . 3 (𝜅𝑈 Se ((𝐴 × 𝐵) × 𝐶))
14 xpord3inddlem.x . . 3 (𝜅𝑋𝐴)
15 xpord3inddlem.y . . 3 (𝜅𝑌𝐵)
16 xpord3inddlem.z . . 3 (𝜅𝑍𝐶)
17 bi2.04 389 . . . . . . 7 ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅𝜃)) ↔ (𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
18173albii 1824 . . . . . 6 (∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅𝜃)) ↔ ∀𝑑𝑒𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
19 19.21v 1943 . . . . . . . 8 (∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
20192albii 1823 . . . . . . 7 (∀𝑑𝑒𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ ∀𝑑𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
21 19.21v 1943 . . . . . . . . 9 (∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
2221albii 1822 . . . . . . . 8 (∀𝑑𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ ∀𝑑(𝜅 → ∀𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
23 19.21v 1943 . . . . . . . 8 (∀𝑑(𝜅 → ∀𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
2422, 23bitri 275 . . . . . . 7 (∀𝑑𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
2520, 24bitri 275 . . . . . 6 (∀𝑑𝑒𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
2618, 25bitri 275 . . . . 5 (∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅𝜃)) ↔ (𝜅 → ∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
271xpord3pred 8133 . . . . . . . . . . . . . . . 16 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
2827adantl 483 . . . . . . . . . . . . . . 15 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
2928eleq2d 2820 . . . . . . . . . . . . . 14 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
3029imbi1d 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
3633, 34, 35otthne 5485 . . . . . . . . . . . . . . . 16 (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
3732, 36anbi12i 628 . . . . . . . . . . . . . . 15 ((⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
3831, 37bitri 275 . . . . . . . . . . . . . 14 (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
3938imbi1i 350 . . . . . . . . . . . . 13 ((⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) → 𝜃))
4030, 39bitrdi 287 . . . . . . . . . . . 12 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) → 𝜃)))
41 impexp 452 . . . . . . . . . . . 12 ((((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
4240, 41bitrdi 287 . . . . . . . . . . 11 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))))
4342albidv 1924 . . . . . . . . . 10 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))))
44432albidv 1927 . . . . . . . . 9 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑑𝑒𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))))
45 r3al 3197 . . . . . . . . . 10 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑑𝑒𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
4645bicomi 223 . . . . . . . . 9 (∀𝑑𝑒𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
4744, 46bitrdi 287 . . . . . . . 8 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
48 ssun1 4171 . . . . . . . . . . . . . . . . . . . 20 Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
49 ssralv 4049 . . . . . . . . . . . . . . . . . . . 20 (Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
5048, 49ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
5150ralimi 3084 . . . . . . . . . . . . . . . . . 18 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
52 ssun1 4171 . . . . . . . . . . . . . . . . . . 19 Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
53 ssralv 4049 . . . . . . . . . . . . . . . . . . 19 (Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . 18 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
5551, 54syl 17 . . . . . . . . . . . . . . . . 17 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
5655ralimi 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 (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
5957, 58ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
6056, 59syl 17 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
6160adantl 483 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
62 predpoirr 6331 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
638, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜅 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
64 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 = 𝑐 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
6564notbid 318 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 = 𝑐 → (¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
6663, 65syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . 22 (𝜅 → (𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)))
6766necon2ad 2956 . . . . . . . . . . . . . . . . . . . . 21 (𝜅 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → 𝑓𝑐))
6867imp 408 . . . . . . . . . . . . . . . . . . . 20 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → 𝑓𝑐)
69683mix3d 1339 . . . . . . . . . . . . . . . . . . 19 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑑𝑎𝑒𝑏𝑓𝑐))
70 pm2.27 42 . . . . . . . . . . . . . . . . . . 19 ((𝑑𝑎𝑒𝑏𝑓𝑐) → (((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → 𝜃))
7169, 70syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → 𝜃))
7271ralimdva 3168 . . . . . . . . . . . . . . . . 17 (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
7372ralimdv 3170 . . . . . . . . . . . . . . . 16 (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
7473ralimdv 3170 . . . . . . . . . . . . . . 15 (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
7574adantr 482 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
7661, 75mpd 15 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
77 ssun2 4172 . . . . . . . . . . . . . . . . . . . . 21 {𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
78 ssralv 4049 . . . . . . . . . . . . . . . . . . . . 21 ({𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
7977, 78ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
8079ralimi 3084 . . . . . . . . . . . . . . . . . . 19 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
81 ssralv 4049 . . . . . . . . . . . . . . . . . . . 20 (Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
8252, 81ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
8380, 82syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
8483ralimi 3084 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
85 ssralv 4049 . . . . . . . . . . . . . . . . . 18 (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
8657, 85ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
8784, 86syl 17 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
88 vex 3479 . . . . . . . . . . . . . . . . . 18 𝑐 ∈ V
89 biidd 262 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑐 → (𝑑𝑎𝑑𝑎))
90 biidd 262 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑐 → (𝑒𝑏𝑒𝑏))
91 neeq1 3004 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑐 → (𝑓𝑐𝑐𝑐))
9289, 90, 913orbi123d 1436 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑐 → ((𝑑𝑎𝑒𝑏𝑓𝑐) ↔ (𝑑𝑎𝑒𝑏𝑐𝑐)))
93 xpord3inddlem.12 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑓 → (𝜒𝜃))
9493equcoms 2024 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑐 → (𝜒𝜃))
9594bicomd 222 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑐 → (𝜃𝜒))
9692, 95imbi12d 345 . . . . . . . . . . . . . . . . . 18 (𝑓 = 𝑐 → (((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒)))
9788, 96ralsn 4684 . . . . . . . . . . . . . . . . 17 (∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒))
98972ralbii 3129 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒))
9987, 98sylib 217 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒))
10099adantl 483 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒))
101 predpoirr 6331 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
1027, 101syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝜅 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
103 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 = 𝑏 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
104103notbid 318 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = 𝑏 → (¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
105102, 104syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . 21 (𝜅 → (𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)))
106105necon2ad 2956 . . . . . . . . . . . . . . . . . . . 20 (𝜅 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑒𝑏))
107106imp 408 . . . . . . . . . . . . . . . . . . 19 ((𝜅𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → 𝑒𝑏)
1081073mix2d 1338 . . . . . . . . . . . . . . . . . 18 ((𝜅𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (𝑑𝑎𝑒𝑏𝑐𝑐))
109 pm2.27 42 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑎𝑒𝑏𝑐𝑐) → (((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒) → 𝜒))
110108, 109syl 17 . . . . . . . . . . . . . . . . 17 ((𝜅𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒) → 𝜒))
111110ralimdva 3168 . . . . . . . . . . . . . . . 16 (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
112111ralimdv 3170 . . . . . . . . . . . . . . 15 (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
113112adantr 482 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
114100, 113mpd 15 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
115 ssun2 4172 . . . . . . . . . . . . . . . . . . . 20 {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
116 ssralv 4049 . . . . . . . . . . . . . . . . . . . 20 ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
117115, 116ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
11851, 117syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
119118ralimi 3084 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
120 ssralv 4049 . . . . . . . . . . . . . . . . . 18 (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
12157, 120ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
122119, 121syl 17 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
123 vex 3479 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ V
124 biidd 262 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑏 → (𝑑𝑎𝑑𝑎))
125 neeq1 3004 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑏 → (𝑒𝑏𝑏𝑏))
126 biidd 262 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑏 → (𝑓𝑐𝑓𝑐))
127124, 125, 1263orbi123d 1436 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑏 → ((𝑑𝑎𝑒𝑏𝑓𝑐) ↔ (𝑑𝑎𝑏𝑏𝑓𝑐)))
128 xpord3inddlem.15 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = 𝑒 → (𝜁𝜃))
129128equcoms 2024 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑏 → (𝜁𝜃))
130129bicomd 222 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑏 → (𝜃𝜁))
131127, 130imbi12d 345 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑏 → (((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁)))
132131ralbidv 3178 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁)))
133123, 132ralsn 4684 . . . . . . . . . . . . . . . . 17 (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁))
134133ralbii 3094 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁))
135122, 134sylib 217 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁))
136135adantl 483 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁))
137683mix3d 1339 . . . . . . . . . . . . . . . . . 18 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑑𝑎𝑏𝑏𝑓𝑐))
138 pm2.27 42 . . . . . . . . . . . . . . . . . 18 ((𝑑𝑎𝑏𝑏𝑓𝑐) → (((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁) → 𝜁))
139137, 138syl 17 . . . . . . . . . . . . . . . . 17 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁) → 𝜁))
140139ralimdva 3168 . . . . . . . . . . . . . . . 16 (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
141140ralimdv 3170 . . . . . . . . . . . . . . 15 (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
142141adantr 482 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑏𝑏𝑓𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
143136, 142mpd 15 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
14476, 114, 1433jca 1129 . . . . . . . . . . . 12 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
145 ssralv 4049 . . . . . . . . . . . . . . . . . . . 20 ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
146115, 145ax-mp 5 . . . . . . . . . . . . . . . . . . 19 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
14780, 146syl 17 . . . . . . . . . . . . . . . . . 18 (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
148147ralimi 3084 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
149 ssralv 4049 . . . . . . . . . . . . . . . . . 18 (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
15057, 149ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
151148, 150syl 17 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
15297ralbii 3094 . . . . . . . . . . . . . . . . . 18 (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏} ((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒))
153 biidd 262 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑏 → (𝑐𝑐𝑐𝑐))
154124, 125, 1533orbi123d 1436 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑏 → ((𝑑𝑎𝑒𝑏𝑐𝑐) ↔ (𝑑𝑎𝑏𝑏𝑐𝑐)))
155 xpord3inddlem.11 . . . . . . . . . . . . . . . . . . . . . 22 (𝑏 = 𝑒 → (𝜓𝜒))
156155equcoms 2024 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = 𝑏 → (𝜓𝜒))
157156bicomd 222 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑏 → (𝜒𝜓))
158154, 157imbi12d 345 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑏 → (((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒) ↔ ((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓)))
159123, 158ralsn 4684 . . . . . . . . . . . . . . . . . 18 (∀𝑒 ∈ {𝑏} ((𝑑𝑎𝑒𝑏𝑐𝑐) → 𝜒) ↔ ((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓))
160152, 159bitri 275 . . . . . . . . . . . . . . . . 17 (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓))
161160ralbii 3094 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓))
162151, 161sylib 217 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓))
163162adantl 483 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓))
164 predpoirr 6331 . . . . . . . . . . . . . . . . . . . . . 22 (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
1656, 164syl 17 . . . . . . . . . . . . . . . . . . . . 21 (𝜅 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
166 eleq1 2822 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = 𝑎 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
167166notbid 318 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑎 → (¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
168165, 167syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . 20 (𝜅 → (𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)))
169168necon2ad 2956 . . . . . . . . . . . . . . . . . . 19 (𝜅 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑑𝑎))
170169imp 408 . . . . . . . . . . . . . . . . . 18 ((𝜅𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → 𝑑𝑎)
1711703mix1d 1337 . . . . . . . . . . . . . . . . 17 ((𝜅𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (𝑑𝑎𝑏𝑏𝑐𝑐))
172 pm2.27 42 . . . . . . . . . . . . . . . . 17 ((𝑑𝑎𝑏𝑏𝑐𝑐) → (((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓) → 𝜓))
173171, 172syl 17 . . . . . . . . . . . . . . . 16 ((𝜅𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓) → 𝜓))
174173ralimdva 3168 . . . . . . . . . . . . . . 15 (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓))
175174adantr 482 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑𝑎𝑏𝑏𝑐𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓))
176163, 175mpd 15 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
177 ssun2 4172 . . . . . . . . . . . . . . . . . 18 {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
178 ssralv 4049 . . . . . . . . . . . . . . . . . 18 ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
179177, 178ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
18056, 179syl 17 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
181 vex 3479 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
182 neeq1 3004 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → (𝑑𝑎𝑎𝑎))
183 biidd 262 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → (𝑒𝑏𝑒𝑏))
184 biidd 262 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → (𝑓𝑐𝑓𝑐))
185182, 183, 1843orbi123d 1436 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑎 → ((𝑑𝑎𝑒𝑏𝑓𝑐) ↔ (𝑎𝑎𝑒𝑏𝑓𝑐)))
186 xpord3inddlem.13 . . . . . . . . . . . . . . . . . . . . 21 (𝑎 = 𝑑 → (𝜏𝜃))
187186equcoms 2024 . . . . . . . . . . . . . . . . . . . 20 (𝑑 = 𝑎 → (𝜏𝜃))
188187bicomd 222 . . . . . . . . . . . . . . . . . . 19 (𝑑 = 𝑎 → (𝜃𝜏))
189185, 188imbi12d 345 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑎 → (((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏)))
1901892ralbidv 3219 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏)))
191181, 190ralsn 4684 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏))
192180, 191sylib 217 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏))
193192adantl 483 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏))
194683mix3d 1339 . . . . . . . . . . . . . . . . . 18 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑎𝑎𝑒𝑏𝑓𝑐))
195 pm2.27 42 . . . . . . . . . . . . . . . . . 18 ((𝑎𝑎𝑒𝑏𝑓𝑐) → (((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) → 𝜏))
196194, 195syl 17 . . . . . . . . . . . . . . . . 17 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) → 𝜏))
197196ralimdva 3168 . . . . . . . . . . . . . . . 16 (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
198197ralimdv 3170 . . . . . . . . . . . . . . 15 (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
199198adantr 482 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
200193, 199mpd 15 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
201 ssralv 4049 . . . . . . . . . . . . . . . . . 18 ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
202177, 201ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
20384, 202syl 17 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
2041892ralbidv 3219 . . . . . . . . . . . . . . . . . 18 (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏)))
205181, 204ralsn 4684 . . . . . . . . . . . . . . . . 17 (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏))
206 biidd 262 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝑐 → (𝑎𝑎𝑎𝑎))
207206, 90, 913orbi123d 1436 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑐 → ((𝑎𝑎𝑒𝑏𝑓𝑐) ↔ (𝑎𝑎𝑒𝑏𝑐𝑐)))
208 xpord3inddlem.16 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = 𝑓 → (𝜎𝜏))
209208bicomd 222 . . . . . . . . . . . . . . . . . . . . 21 (𝑐 = 𝑓 → (𝜏𝜎))
210209equcoms 2024 . . . . . . . . . . . . . . . . . . . 20 (𝑓 = 𝑐 → (𝜏𝜎))
211207, 210imbi12d 345 . . . . . . . . . . . . . . . . . . 19 (𝑓 = 𝑐 → (((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) ↔ ((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎)))
21288, 211ralsn 4684 . . . . . . . . . . . . . . . . . 18 (∀𝑓 ∈ {𝑐} ((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) ↔ ((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎))
213212ralbii 3094 . . . . . . . . . . . . . . . . 17 (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎))
214205, 213bitri 275 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎))
215203, 214sylib 217 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎))
216215adantl 483 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎))
2171073mix2d 1338 . . . . . . . . . . . . . . . . 17 ((𝜅𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (𝑎𝑎𝑒𝑏𝑐𝑐))
218 pm2.27 42 . . . . . . . . . . . . . . . . 17 ((𝑎𝑎𝑒𝑏𝑐𝑐) → (((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎) → 𝜎))
219217, 218syl 17 . . . . . . . . . . . . . . . 16 ((𝜅𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎) → 𝜎))
220219ralimdva 3168 . . . . . . . . . . . . . . 15 (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
221220adantr 482 . . . . . . . . . . . . . 14 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑒𝑏𝑐𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
222216, 221mpd 15 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)
223176, 200, 2223jca 1129 . . . . . . . . . . . 12 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
224 ssralv 4049 . . . . . . . . . . . . . . . . 17 ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)))
225177, 224ax-mp 5 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
226119, 225syl 17 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃))
2271892ralbidv 3219 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝑎 → (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏)))
228181, 227ralsn 4684 . . . . . . . . . . . . . . . 16 (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏))
229 biidd 262 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑏 → (𝑎𝑎𝑎𝑎))
230229, 125, 1263orbi123d 1436 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑏 → ((𝑎𝑎𝑒𝑏𝑓𝑐) ↔ (𝑎𝑎𝑏𝑏𝑓𝑐)))
231 equcomi 2021 . . . . . . . . . . . . . . . . . . . 20 (𝑒 = 𝑏𝑏 = 𝑒)
232 xpord3inddlem.14 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑒 → (𝜂𝜏))
233 bicom1 220 . . . . . . . . . . . . . . . . . . . 20 ((𝜂𝜏) → (𝜏𝜂))
234231, 232, 2333syl 18 . . . . . . . . . . . . . . . . . . 19 (𝑒 = 𝑏 → (𝜏𝜂))
235230, 234imbi12d 345 . . . . . . . . . . . . . . . . . 18 (𝑒 = 𝑏 → (((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) ↔ ((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂)))
236235ralbidv 3178 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂)))
237123, 236ralsn 4684 . . . . . . . . . . . . . . . 16 (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑒𝑏𝑓𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂))
238228, 237bitri 275 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂))
239226, 238sylib 217 . . . . . . . . . . . . . 14 (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂))
240239adantl 483 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂))
241683mix3d 1339 . . . . . . . . . . . . . . . 16 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑎𝑎𝑏𝑏𝑓𝑐))
242 pm2.27 42 . . . . . . . . . . . . . . . 16 ((𝑎𝑎𝑏𝑏𝑓𝑐) → (((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂) → 𝜂))
243241, 242syl 17 . . . . . . . . . . . . . . 15 ((𝜅𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂) → 𝜂))
244243ralimdva 3168 . . . . . . . . . . . . . 14 (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
245244adantr 482 . . . . . . . . . . . . 13 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎𝑎𝑏𝑏𝑓𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
246240, 245mpd 15 . . . . . . . . . . . 12 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)
247144, 223, 2463jca 1129 . . . . . . . . . . 11 ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃)) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
248247ex 414 . . . . . . . . . 10 (𝜅 → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)))
249248adantr 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 (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))
251249, 250syld 47 . . . . . . . 8 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑𝑎𝑒𝑏𝑓𝑐) → 𝜃) → 𝜑))
25247, 251sylbid 239 . . . . . . 7 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) → 𝜑))
253252expcom 415 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝜅 → (∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) → 𝜑)))
254253a2d 29 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((𝜅 → ∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) → (𝜅𝜑)))
25526, 254biimtrid 241 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (∀𝑑𝑒𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅𝜃)) → (𝜅𝜑)))
256 xpord3inddlem.10 . . . . 5 (𝑎 = 𝑑 → (𝜑𝜓))
257256imbi2d 341 . . . 4 (𝑎 = 𝑑 → ((𝜅𝜑) ↔ (𝜅𝜓)))
258155imbi2d 341 . . . 4 (𝑏 = 𝑒 → ((𝜅𝜓) ↔ (𝜅𝜒)))
25993imbi2d 341 . . . 4 (𝑐 = 𝑓 → ((𝜅𝜒) ↔ (𝜅𝜃)))
260 xpord3inddlem.17 . . . . 5 (𝑎 = 𝑋 → (𝜑𝜌))
261260imbi2d 341 . . . 4 (𝑎 = 𝑋 → ((𝜅𝜑) ↔ (𝜅𝜌)))
262 xpord3inddlem.18 . . . . 5 (𝑏 = 𝑌 → (𝜌𝜇))
263262imbi2d 341 . . . 4 (𝑏 = 𝑌 → ((𝜅𝜌) ↔ (𝜅𝜇)))
264 xpord3inddlem.19 . . . . 5 (𝑐 = 𝑍 → (𝜇𝜆))
265264imbi2d 341 . . . 4 (𝑐 = 𝑍 → ((𝜅𝜇) ↔ (𝜅𝜆)))
266255, 257, 258, 259, 261, 263, 265frpoins3xp3g 8122 . . 3 (((𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋𝐴𝑌𝐵𝑍𝐶)) → (𝜅𝜆))
2675, 9, 13, 14, 15, 16, 266syl33anc 1386 . 2 (𝜅 → (𝜅𝜆))
268267pm2.43i 52 1 (𝜅𝜆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 846  w3o 1087  w3a 1088  wal 1540   = wceq 1542  wcel 2107  wne 2941  wral 3062  cdif 3944  cun 3945  wss 3947  {csn 4627  cotp 4635   class class class wbr 5147  {copab 5209   Po wpo 5585   Fr wfr 5627   Se wse 5628   × cxp 5673  Predcpred 6296  cfv 6540  1st c1st 7968  2nd c2nd 7969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7720
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-ot 4636  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-po 5587  df-fr 5630  df-se 5631  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-iota 6492  df-fun 6542  df-fv 6548  df-1st 7970  df-2nd 7971
This theorem is referenced by:  xpord3indd  8136
  Copyright terms: Public domain W3C validator