xpord3inddlem - Metamath Proof Explorer

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

Theorem xpord3inddlem 8156

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	⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1^st ‘(1^st ‘𝑥))𝑅(1^st ‘(1^st ‘𝑦)) ∨ (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑦))) ∧ ((2^nd ‘(1^st ‘𝑥))𝑆(2^nd ‘(1^st ‘𝑦)) ∨ (2^nd ‘(1^st ‘𝑥)) = (2^nd ‘(1^st ‘𝑦))) ∧ ((2^nd ‘𝑥)𝑇(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
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**
Step	Hyp	Ref	Expression
1		xpord3.1	. . . 4 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1^st ‘(1^st ‘𝑥))𝑅(1^st ‘(1^st ‘𝑦)) ∨ (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑦))) ∧ ((2^nd ‘(1^st ‘𝑥))𝑆(2^nd ‘(1^st ‘𝑦)) ∨ (2^nd ‘(1^st ‘𝑥)) = (2^nd ‘(1^st ‘𝑦))) ∧ ((2^nd ‘𝑥)𝑇(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
2		xpord3inddlem.1	. . . 4 ⊢ (𝜅 → 𝑅 Fr 𝐴)
3		xpord3inddlem.4	. . . 4 ⊢ (𝜅 → 𝑆 Fr 𝐵)
4		xpord3inddlem.7	. . . 4 ⊢ (𝜅 → 𝑇 Fr 𝐶)
5	1, 2, 3, 4	frxp3 8153	. . 3 ⊢ (𝜅 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
6		xpord3inddlem.2	. . . 4 ⊢ (𝜅 → 𝑅 Po 𝐴)
7		xpord3inddlem.5	. . . 4 ⊢ (𝜅 → 𝑆 Po 𝐵)
8		xpord3inddlem.8	. . . 4 ⊢ (𝜅 → 𝑇 Po 𝐶)
9	1, 6, 7, 8	poxp3 8152	. . 3 ⊢ (𝜅 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))
10		xpord3inddlem.3	. . . 4 ⊢ (𝜅 → 𝑅 Se 𝐴)
11		xpord3inddlem.6	. . . 4 ⊢ (𝜅 → 𝑆 Se 𝐵)
12		xpord3inddlem.9	. . . 4 ⊢ (𝜅 → 𝑇 Se 𝐶)
13	1, 10, 11, 12	sexp3 8155	. . 3 ⊢ (𝜅 → 𝑈 Se ((𝐴 × 𝐵) × 𝐶))
14		xpord3inddlem.x	. . 3 ⊢ (𝜅 → 𝑋 ∈ 𝐴)
15		xpord3inddlem.y	. . 3 ⊢ (𝜅 → 𝑌 ∈ 𝐵)
16		xpord3inddlem.z	. . 3 ⊢ (𝜅 → 𝑍 ∈ 𝐶)
17		bi2.04 392	. . . . . . 7 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅 → 𝜃)) ↔ (𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
18	17	3albii 1854	. . . . . 6 ⊢ (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅 → 𝜃)) ↔ ∀𝑑∀𝑒∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
19		19.21v 1972	. . . . . . . 8 ⊢ (∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
20	19	2albii 1853	. . . . . . 7 ⊢ (∀𝑑∀𝑒∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ ∀𝑑∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
21		19.21v 1972	. . . . . . . . 9 ⊢ (∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
22	21	albii 1852	. . . . . . . 8 ⊢ (∀𝑑∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ ∀𝑑(𝜅 → ∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
23		19.21v 1972	. . . . . . . 8 ⊢ (∀𝑑(𝜅 → ∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
24	22, 23	bitri 278	. . . . . . 7 ⊢ (∀𝑑∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
25	20, 24	bitri 278	. . . . . 6 ⊢ (∀𝑑∀𝑒∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
26	18, 25	bitri 278	. . . . 5 ⊢ (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅 → 𝜃)) ↔ (𝜅 → ∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
27	1	xpord3pred 8154	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
28	27	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
29	28	eleq2d 2851	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
30	29	imbi1d 344	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) → 𝜃)))
31		eldifsn 4755	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
32		otelxp 5707	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
33		vex 3461	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
34		vex 3461	. . . . . . . . . . . . . . . . 17 ⊢ 𝑒 ∈ V
35		vex 3461	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
36	33, 34, 35	otthne 5470	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
37	32, 36	anbi12i 640	. . . . . . . . . . . . . . 15 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
38	31, 37	bitri 278	. . . . . . . . . . . . . 14 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
39	38	imbi1i 352	. . . . . . . . . . . . 13 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃))
40	30, 39	bitrdi 290	. . . . . . . . . . . 12 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃)))
41		impexp 456	. . . . . . . . . . . 12 ⊢ ((((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
42	40, 41	bitrdi 290	. . . . . . . . . . 11 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
43	42	albidv 1953	. . . . . . . . . 10 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
44	43	2albidv 1956	. . . . . . . . 9 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
45		r3al 3205	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
46	45	bicomi 227	. . . . . . . . 9 ⊢ (∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
47	44, 46	bitrdi 290	. . . . . . . 8 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
48		ssun1 4131	. . . . . . . . . . . . . . . . . . . 20 ⊢ Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
49		ssralv 4007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
50	48, 49	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
51	50	ralimi 3104	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
52		ssun1 4131	. . . . . . . . . . . . . . . . . . 19 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
53		ssralv 4007	. . . . . . . . . . . . . . . . . . 19 ⊢ (Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
54	52, 53	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
55	51, 54	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
56	55	ralimi 3104	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
57		ssun1 4131	. . . . . . . . . . . . . . . . 17 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
58		ssralv 4007	. . . . . . . . . . . . . . . . 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 18	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
61	60	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
62		predpoirr 6338	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
63	8, 62	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜅 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
64		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
65	64	notbid 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑐 → (¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
66	63, 65	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜅 → (𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)))
67	66	necon2ad 2975	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜅 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → 𝑓 ≠ 𝑐))
68	67	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → 𝑓 ≠ 𝑐)
69	68	3mix3d 1357	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
70		pm2.27 43	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
71	69, 70	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
72	71	ralimdva 3179	. . . . . . . . . . . . . . . . 17 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
73	72	ralimdv 3181	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
74	73	ralimdv 3181	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
75	74	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
76	61, 75	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
77		ssun2 4132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
78		ssralv 4007	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
79	77, 78	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
80	79	ralimi 3104	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
81		ssralv 4007	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
82	52, 81	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
83	80, 82	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
84	83	ralimi 3104	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
85		ssralv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
86	57, 85	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
87	84, 86	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
88		vex 3461	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑐 ∈ V
89		biidd 265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
90		biidd 265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
91		neeq1 3022	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝑓 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
92	89, 90, 91	3orbi123d 1463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑐 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
93		xpord3inddlem.12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))
94	93	equcoms 2053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝜒 ↔ 𝜃))
95	94	bicomd 226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑐 → (𝜃 ↔ 𝜒))
96	92, 95	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑐 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)))
97	88, 96	ralsn 4649	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
98	97	2ralbii 3142	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
99	87, 98	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
100	99	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
101		predpoirr 6338	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
102	7, 101	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜅 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
103		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
104	103	notbid 321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = 𝑏 → (¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
105	102, 104	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜅 → (𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)))
106	105	necon2ad 2975	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜅 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑒 ≠ 𝑏))
107	106	imp 412	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → 𝑒 ≠ 𝑏)
108	107	3mix2d 1356	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
109		pm2.27 43	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
110	108, 109	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
111	110	ralimdva 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
112	111	ralimdv 3181	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
113	112	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
114	100, 113	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
115		ssun2 4132	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
116		ssralv 4007	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
117	115, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
118	51, 117	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
119	118	ralimi 3104	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
120		ssralv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
121	57, 120	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
122	119, 121	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
123		vex 3461	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
124		biidd 265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
125		neeq1 3022	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑒 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏))
126		biidd 265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
127	124, 125, 126	3orbi123d 1463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
128		xpord3inddlem.15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))
129	128	equcoms 2053	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝜁 ↔ 𝜃))
130	129	bicomd 226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → (𝜃 ↔ 𝜁))
131	127, 130	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
132	131	ralbidv 3190	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
133	123, 132	ralsn 4649	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
134	133	ralbii 3113	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
135	122, 134	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
136	135	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
137	68	3mix3d 1357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
138		pm2.27 43	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁))
139	137, 138	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁))
140	139	ralimdva 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
141	140	ralimdv 3181	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
142	141	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
143	136, 142	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
144	76, 114, 143	3jca 1146	. . . . . . . . . . . 12 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
145		ssralv 4007	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
146	115, 145	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
147	80, 146	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
148	147	ralimi 3104	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
149		ssralv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
150	57, 149	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
151	148, 150	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
152	97	ralbii 3113	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
153		biidd 265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑐 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
154	124, 125, 153	3orbi123d 1463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
155		xpord3inddlem.11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))
156	155	equcoms 2053	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝜓 ↔ 𝜒))
157	156	bicomd 226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → (𝜒 ↔ 𝜓))
158	154, 157	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)))
159	123, 158	ralsn 4649	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
160	152, 159	bitri 278	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
161	160	ralbii 3113	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
162	151, 161	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
163	162	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
164		predpoirr 6338	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
165	6, 164	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜅 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
166		eleq1 2853	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = 𝑎 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
167	166	notbid 321	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
168	165, 167	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜅 → (𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)))
169	168	necon2ad 2975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜅 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑑 ≠ 𝑎))
170	169	imp 412	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → 𝑑 ≠ 𝑎)
171	170	3mix1d 1355	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
172		pm2.27 43	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
173	171, 172	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
174	173	ralimdva 3179	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓))
175	174	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓))
176	163, 175	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
177		ssun2 4132	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
178		ssralv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
179	177, 178	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
180	56, 179	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
181		vex 3461	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ∈ V
182		neeq1 3022	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝑑 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
183		biidd 265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
184		biidd 265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
185	182, 183, 184	3orbi123d 1463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑎 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
186		xpord3inddlem.13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))
187	186	equcoms 2053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝜏 ↔ 𝜃))
188	187	bicomd 226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑎 → (𝜃 ↔ 𝜏))
189	185, 188	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑎 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
190	189	2ralbidv 3231	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
191	181, 190	ralsn 4649	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
192	180, 191	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
193	192	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
194	68	3mix3d 1357	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
195		pm2.27 43	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏))
196	194, 195	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏))
197	196	ralimdva 3179	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
198	197	ralimdv 3181	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
199	198	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
200	193, 199	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
201		ssralv 4007	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
202	177, 201	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
203	84, 202	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
204	189	2ralbidv 3231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
205	181, 204	ralsn 4649	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
206		biidd 265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑐 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
207	206, 90, 91	3orbi123d 1463	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
208		xpord3inddlem.16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))
209	208	bicomd 226	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑓 → (𝜏 ↔ 𝜎))
210	209	equcoms 2053	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝜏 ↔ 𝜎))
211	207, 210	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑐 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)))
212	88, 211	ralsn 4649	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
213	212	ralbii 3113	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
214	205, 213	bitri 278	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
215	203, 214	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
216	215	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
217	107	3mix2d 1356	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
218		pm2.27 43	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎))
219	217, 218	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎))
220	219	ralimdva 3179	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
221	220	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
222	216, 221	mpd 16	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)
223	176, 200, 222	3jca 1146	. . . . . . . . . . . 12 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
224		ssralv 4007	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
225	177, 224	ax-mp 5	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
226	119, 225	syl 18	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
227	189	2ralbidv 3231	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
228	181, 227	ralsn 4649	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
229		biidd 265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
230	229, 125, 126	3orbi123d 1463	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
231		equcomi 2050	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → 𝑏 = 𝑒)
232		xpord3inddlem.14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))
233		bicom1 224	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜂 ↔ 𝜏) → (𝜏 ↔ 𝜂))
234	231, 232, 233	3syl 19	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → (𝜏 ↔ 𝜂))
235	230, 234	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑏 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
236	235	ralbidv 3190	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
237	123, 236	ralsn 4649	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
238	228, 237	bitri 278	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
239	226, 238	sylib 221	. . . . . . . . . . . . . 14 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
240	239	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
241	68	3mix3d 1357	. . . . . . . . . . . . . . . 16 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
242		pm2.27 43	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂))
243	241, 242	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂))
244	243	ralimdva 3179	. . . . . . . . . . . . . 14 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
245	244	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
246	240, 245	mpd 16	. . . . . . . . . . . 12 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)
247	144, 223, 246	3jca 1146	. . . . . . . . . . 11 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
248	247	ex 418	. . . . . . . . . 10 ⊢ (𝜅 → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)))
249	248	adantr 486	. . . . . . . . 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 48	. . . . . . . 8 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜑))
252	47, 251	sylbid 243	. . . . . . 7 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) → 𝜑))
253	252	expcom 419	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝜅 → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) → 𝜑)))
254	253	a2d 30	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝜅 → ∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) → (𝜅 → 𝜑)))
255	26, 254	biimtrid 245	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅 → 𝜃)) → (𝜅 → 𝜑)))
256		xpord3inddlem.10	. . . . 5 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))
257	256	imbi2d 343	. . . 4 ⊢ (𝑎 = 𝑑 → ((𝜅 → 𝜑) ↔ (𝜅 → 𝜓)))
258	155	imbi2d 343	. . . 4 ⊢ (𝑏 = 𝑒 → ((𝜅 → 𝜓) ↔ (𝜅 → 𝜒)))
259	93	imbi2d 343	. . . 4 ⊢ (𝑐 = 𝑓 → ((𝜅 → 𝜒) ↔ (𝜅 → 𝜃)))
260		xpord3inddlem.17	. . . . 5 ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))
261	260	imbi2d 343	. . . 4 ⊢ (𝑎 = 𝑋 → ((𝜅 → 𝜑) ↔ (𝜅 → 𝜌)))
262		xpord3inddlem.18	. . . . 5 ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))
263	262	imbi2d 343	. . . 4 ⊢ (𝑏 = 𝑌 → ((𝜅 → 𝜌) ↔ (𝜅 → 𝜇)))
264		xpord3inddlem.19	. . . . 5 ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))
265	264	imbi2d 343	. . . 4 ⊢ (𝑐 = 𝑍 → ((𝜅 → 𝜇) ↔ (𝜅 → 𝜆)))
266	255, 257, 258, 259, 261, 263, 265	frpoins3xp3g 8143	. . 3 ⊢ (((𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → (𝜅 → 𝜆))
267	5, 9, 13, 14, 15, 16, 266	syl33anc 1412	. 2 ⊢ (𝜅 → (𝜅 → 𝜆))
268	267	pm2.43i 53	1 ⊢ (𝜅 → 𝜆)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 ∀wal 1568 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 ∀wral 3081 ∖ cdif 3903 ∪ cun 3904 ⊆ wss 3906 {csn 4591 ⟨cotp 4599 class class class wbr 5111 {copab 5175 Po wpo 5569 Fr wfr 5613 Se wse 5614 × cxp 5661 Predcpred 6305 ‘cfv 6540 1^st c1st 7990 2^nd c2nd 7991

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-ot 4600 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-po 5571 df-fr 5616 df-se 5617 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-iota 6496 df-fun 6542 df-fv 6548 df-1st 7992 df-2nd 7993

This theorem is used by: xpord3indd 8157

W3C validator