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 8179

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 8176	. . 3 ⊢ (𝜅 → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
6		xpord3inddlem.2	. . . 4 ⊢ (𝜅 → 𝑅 Po 𝐴)
7		xpord3inddlem.5	. . . 4 ⊢ (𝜅 → 𝑆 Po 𝐵)
8		xpord3inddlem.8	. . . 4 ⊢ (𝜅 → 𝑇 Po 𝐶)
9	1, 6, 7, 8	poxp3 8175	. . 3 ⊢ (𝜅 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))
10		xpord3inddlem.3	. . . 4 ⊢ (𝜅 → 𝑅 Se 𝐴)
11		xpord3inddlem.6	. . . 4 ⊢ (𝜅 → 𝑆 Se 𝐵)
12		xpord3inddlem.9	. . . 4 ⊢ (𝜅 → 𝑇 Se 𝐶)
13	1, 10, 11, 12	sexp3 8178	. . 3 ⊢ (𝜅 → 𝑈 Se ((𝐴 × 𝐵) × 𝐶))
14		xpord3inddlem.x	. . 3 ⊢ (𝜅 → 𝑋 ∈ 𝐴)
15		xpord3inddlem.y	. . 3 ⊢ (𝜅 → 𝑌 ∈ 𝐵)
16		xpord3inddlem.z	. . 3 ⊢ (𝜅 → 𝑍 ∈ 𝐶)
17		bi2.04 387	. . . . . . 7 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅 → 𝜃)) ↔ (𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
18	17	3albii 1821	. . . . . 6 ⊢ (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅 → 𝜃)) ↔ ∀𝑑∀𝑒∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
19		19.21v 1939	. . . . . . . 8 ⊢ (∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
20	19	2albii 1820	. . . . . . 7 ⊢ (∀𝑑∀𝑒∀𝑓(𝜅 → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ ∀𝑑∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
21		19.21v 1939	. . . . . . . . 9 ⊢ (∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ (𝜅 → ∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
22	21	albii 1819	. . . . . . . 8 ⊢ (∀𝑑∀𝑒(𝜅 → ∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) ↔ ∀𝑑(𝜅 → ∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)))
23		19.21v 1939	. . . . . . . 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 8177	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
28	27	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
29	28	eleq2d 2827	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
30	29	imbi1d 341	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) → 𝜃)))
31		eldifsn 4786	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
32		otelxp 5729	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
33		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
34		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑒 ∈ V
35		vex 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
36	33, 34, 35	otthne 5491	. . . . . . . . . . . . . . . 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 349	. . . . . . . . . . . . 13 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃))
40	30, 39	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃)))
41		impexp 450	. . . . . . . . . . . 12 ⊢ ((((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
42	40, 41	bitrdi 287	. . . . . . . . . . 11 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → ((⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
43	42	albidv 1920	. . . . . . . . . 10 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
44	43	2albidv 1923	. . . . . . . . 9 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
45		r3al 3197	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
46	45	bicomi 224	. . . . . . . . 9 ⊢ (∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
47	44, 46	bitrdi 287	. . . . . . . 8 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
48		ssun1 4178	. . . . . . . . . . . . . . . . . . . 20 ⊢ Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
49		ssralv 4052	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
50	48, 49	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
51	50	ralimi 3083	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
52		ssun1 4178	. . . . . . . . . . . . . . . . . . 19 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
53		ssralv 4052	. . . . . . . . . . . . . . . . . . 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 3083	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
57		ssun1 4178	. . . . . . . . . . . . . . . . 17 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
58		ssralv 4052	. . . . . . . . . . . . . . . . 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 481	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
62		predpoirr 6354	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
63	8, 62	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜅 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
64		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
65	64	notbid 318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑐 → (¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
66	63, 65	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜅 → (𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)))
67	66	necon2ad 2955	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜅 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → 𝑓 ≠ 𝑐))
68	67	imp 406	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → 𝑓 ≠ 𝑐)
69	68	3mix3d 1339	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
70		pm2.27 42	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
71	69, 70	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐)) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
72	71	ralimdva 3167	. . . . . . . . . . . . . . . . 17 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
73	72	ralimdv 3169	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
74	73	ralimdv 3169	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
75	74	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃))
76	61, 75	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
77		ssun2 4179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
78		ssralv 4052	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
79	77, 78	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
80	79	ralimi 3083	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
81		ssralv 4052	. . . . . . . . . . . . . . . . . . . 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 3083	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
85		ssralv 4052	. . . . . . . . . . . . . . . . . 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 3484	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑐 ∈ V
89		biidd 262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
90		biidd 262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
91		neeq1 3003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝑓 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
92	89, 90, 91	3orbi123d 1437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑐 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
93		xpord3inddlem.12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))
94	93	equcoms 2019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝜒 ↔ 𝜃))
95	94	bicomd 223	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑐 → (𝜃 ↔ 𝜒))
96	92, 95	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 = 𝑐 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)))
97	88, 96	ralsn 4681	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
98	97	2ralbii 3128	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
99	87, 98	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
100	99	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
101		predpoirr 6354	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
102	7, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜅 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
103		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
104	103	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = 𝑏 → (¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
105	102, 104	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜅 → (𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)))
106	105	necon2ad 2955	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜅 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑒 ≠ 𝑏))
107	106	imp 406	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → 𝑒 ≠ 𝑏)
108	107	3mix2d 1338	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
109		pm2.27 42	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
110	108, 109	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜅 ∧ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏)) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
111	110	ralimdva 3167	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
112	111	ralimdv 3169	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
113	112	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒))
114	100, 113	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
115		ssun2 4179	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
116		ssralv 4052	. . . . . . . . . . . . . . . . . . . 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 3083	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
120		ssralv 4052	. . . . . . . . . . . . . . . . . 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 3484	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
124		biidd 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
125		neeq1 3003	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑒 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏))
126		biidd 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
127	124, 125, 126	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
128		xpord3inddlem.15	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))
129	128	equcoms 2019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝜁 ↔ 𝜃))
130	129	bicomd 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → (𝜃 ↔ 𝜁))
131	127, 130	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
132	131	ralbidv 3178	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
133	123, 132	ralsn 4681	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
134	133	ralbii 3093	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
135	122, 134	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
136	135	adantl 481	. . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
141	140	ralimdv 3169	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
142	141	adantr 480	. . . . . . . . . . . . . 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 4052	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
146	115, 145	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
147	80, 146	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
148	147	ralimi 3083	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
149		ssralv 4052	. . . . . . . . . . . . . . . . . 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 3093	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
153		biidd 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝑐 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
154	124, 125, 153	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
155		xpord3inddlem.11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))
156	155	equcoms 2019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑏 → (𝜓 ↔ 𝜒))
157	156	bicomd 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → (𝜒 ↔ 𝜓))
158	154, 157	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)))
159	123, 158	ralsn 4681	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
160	152, 159	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
161	160	ralbii 3093	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
162	151, 161	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
163	162	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
164		predpoirr 6354	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
165	6, 164	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜅 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
166		eleq1 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = 𝑎 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
167	166	notbid 318	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑎 → (¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
168	165, 167	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜅 → (𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)))
169	168	necon2ad 2955	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜅 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑑 ≠ 𝑎))
170	169	imp 406	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → 𝑑 ≠ 𝑎)
171	170	3mix1d 1337	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
172		pm2.27 42	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
173	171, 172	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜅 ∧ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎)) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
174	173	ralimdva 3167	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓))
175	174	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓))
176	163, 175	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
177		ssun2 4179	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
178		ssralv 4052	. . . . . . . . . . . . . . . . . 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 3484	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ∈ V
182		neeq1 3003	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝑑 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
183		biidd 262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
184		biidd 262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
185	182, 183, 184	3orbi123d 1437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑎 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
186		xpord3inddlem.13	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))
187	186	equcoms 2019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑎 → (𝜏 ↔ 𝜃))
188	187	bicomd 223	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑎 → (𝜃 ↔ 𝜏))
189	185, 188	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑎 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
190	189	2ralbidv 3221	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
191	181, 190	ralsn 4681	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
192	180, 191	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
193	192	adantl 481	. . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . . 16 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
198	197	ralimdv 3169	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
199	198	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏))
200	193, 199	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜅 ∧ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
201		ssralv 4052	. . . . . . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
205	181, 204	ralsn 4681	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
206		biidd 262	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑐 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
207	206, 90, 91	3orbi123d 1437	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
208		xpord3inddlem.16	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))
209	208	bicomd 223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑓 → (𝜏 ↔ 𝜎))
210	209	equcoms 2019	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑐 → (𝜏 ↔ 𝜎))
211	207, 210	imbi12d 344	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = 𝑐 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)))
212	88, 211	ralsn 4681	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
213	212	ralbii 3093	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
214	205, 213	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
215	203, 214	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
216	215	adantl 481	. . . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . . 15 ⊢ (𝜅 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
221	220	adantr 480	. . . . . . . . . . . . . 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 4052	. . . . . . . . . . . . . . . . 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 3221	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
228	181, 227	ralsn 4681	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
229		biidd 262	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
230	229, 125, 126	3orbi123d 1437	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
231		equcomi 2016	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = 𝑏 → 𝑏 = 𝑒)
232		xpord3inddlem.14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))
233		bicom1 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜂 ↔ 𝜏) → (𝜏 ↔ 𝜂))
234	231, 232, 233	3syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = 𝑏 → (𝜏 ↔ 𝜂))
235	230, 234	imbi12d 344	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 = 𝑏 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
236	235	ralbidv 3178	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
237	123, 236	ralsn 4681	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
238	228, 237	bitri 275	. . . . . . . . . . . . . . 15 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
239	226, 238	sylib 218	. . . . . . . . . . . . . 14 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
240	239	adantl 481	. . . . . . . . . . . . 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 3167	. . . . . . . . . . . . . 14 ⊢ (𝜅 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
245	244	adantr 480	. . . . . . . . . . . . 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 412	. . . . . . . . . 10 ⊢ (𝜅 → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)))
249	248	adantr 480	. . . . . . . . 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 240	. . . . . . 7 ⊢ ((𝜅 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) → 𝜑))
253	252	expcom 413	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝜅 → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃) → 𝜑)))
254	253	a2d 29	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝜅 → ∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → 𝜃)) → (𝜅 → 𝜑)))
255	26, 254	biimtrid 242	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(⟨𝑑, 𝑒, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) → (𝜅 → 𝜃)) → (𝜅 → 𝜑)))
256		xpord3inddlem.10	. . . . 5 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))
257	256	imbi2d 340	. . . 4 ⊢ (𝑎 = 𝑑 → ((𝜅 → 𝜑) ↔ (𝜅 → 𝜓)))
258	155	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝑒 → ((𝜅 → 𝜓) ↔ (𝜅 → 𝜒)))
259	93	imbi2d 340	. . . 4 ⊢ (𝑐 = 𝑓 → ((𝜅 → 𝜒) ↔ (𝜅 → 𝜃)))
260		xpord3inddlem.17	. . . . 5 ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))
261	260	imbi2d 340	. . . 4 ⊢ (𝑎 = 𝑋 → ((𝜅 → 𝜑) ↔ (𝜅 → 𝜌)))
262		xpord3inddlem.18	. . . . 5 ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))
263	262	imbi2d 340	. . . 4 ⊢ (𝑏 = 𝑌 → ((𝜅 → 𝜌) ↔ (𝜅 → 𝜇)))
264		xpord3inddlem.19	. . . . 5 ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))
265	264	imbi2d 340	. . . 4 ⊢ (𝑐 = 𝑍 → ((𝜅 → 𝜇) ↔ (𝜅 → 𝜆)))
266	255, 257, 258, 259, 261, 263, 265	frpoins3xp3g 8166	. . 3 ⊢ (((𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → (𝜅 → 𝜆))
267	5, 9, 13, 14, 15, 16, 266	syl33anc 1387	. 2 ⊢ (𝜅 → (𝜅 → 𝜆))
268	267	pm2.43i 52	1 ⊢ (𝜅 → 𝜆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∨ w3o 1086 ∧ w3a 1087 ∀wal 1538 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∖ cdif 3948 ∪ cun 3949 ⊆ wss 3951 {csn 4626 ⟨cotp 4634 class class class wbr 5143 {copab 5205 Po wpo 5590 Fr wfr 5634 Se wse 5635 × cxp 5683 Predcpred 6320 ‘cfv 6561 1^st c1st 8012 2^nd c2nd 8013

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-ot 4635 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-po 5592 df-fr 5637 df-se 5638 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-iota 6514 df-fun 6563 df-fv 6569 df-1st 8014 df-2nd 8015

This theorem is referenced by: xpord3indd 8180

W3C validator