xpord3ind - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > xpord3ind		Structured version Visualization version GIF version

Theorem xpord3ind 33727

Description: Induction over the triple cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024.)

**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 ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
xpord3ind.1	⊢ 𝑅 Fr 𝐴
xpord3ind.2	⊢ 𝑅 Po 𝐴
xpord3ind.3	⊢ 𝑅 Se 𝐴
xpord3ind.4	⊢ 𝑆 Fr 𝐵
xpord3ind.5	⊢ 𝑆 Po 𝐵
xpord3ind.6	⊢ 𝑆 Se 𝐵
xpord3ind.7	⊢ 𝑇 Fr 𝐶
xpord3ind.8	⊢ 𝑇 Po 𝐶
xpord3ind.9	⊢ 𝑇 Se 𝐶
xpord3ind.10	⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))
xpord3ind.11	⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))
xpord3ind.12	⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))
xpord3ind.13	⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))
xpord3ind.14	⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))
xpord3ind.15	⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))
xpord3ind.16	⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))
xpord3ind.17	⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))
xpord3ind.18	⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))
xpord3ind.19	⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))
xpord3ind.i	⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))

**Assertion**
Ref	Expression
xpord3ind	⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → 𝜆)

Distinct variable groups: 𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝜓,𝑎 𝜌,𝑎 𝜃,𝑎 𝑥,𝐴,𝑦 𝐵,𝑎,𝑏,𝑐 𝜒,𝑏 𝑏,𝑑,𝐵,𝑒,𝑓 𝜇,𝑏 𝜃,𝑏 𝑥,𝐵,𝑦 𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝜆,𝑐 𝜃,𝑐 𝑥,𝐶,𝑦 𝜒,𝑓 𝑒,𝑑,𝑓 𝜑,𝑑 𝜏,𝑑 𝜂,𝑒 𝑒,𝑓 𝜓,𝑒 𝜁,𝑒 𝜎,𝑓 𝑅,𝑑,𝑒,𝑓 𝑥,𝑅,𝑦 𝑆,𝑑,𝑒,𝑓 𝑥,𝑆,𝑦 𝑇,𝑑,𝑒,𝑓 𝑥,𝑇,𝑦 𝑈,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓 𝑋,𝑎,𝑏,𝑐 𝑥,𝑦 𝑌,𝑏,𝑐 𝑍,𝑐 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑐) 𝜓(𝑥,𝑦,𝑓,𝑏,𝑐,𝑑) 𝜒(𝑥,𝑦,𝑒,𝑎,𝑐,𝑑) 𝜃(𝑥,𝑦,𝑒,𝑓,𝑑) 𝜏(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑐) 𝜂(𝑥,𝑦,𝑓,𝑎,𝑏,𝑐,𝑑) 𝜁(𝑥,𝑦,𝑓,𝑎,𝑏,𝑐,𝑑) 𝜎(𝑥,𝑦,𝑒,𝑎,𝑏,𝑐,𝑑) 𝜌(𝑥,𝑦,𝑒,𝑓,𝑏,𝑐,𝑑) 𝜇(𝑥,𝑦,𝑒,𝑓,𝑎,𝑐,𝑑) 𝜆(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑑) 𝑅(𝑎,𝑏,𝑐) 𝑆(𝑎,𝑏,𝑐) 𝑇(𝑎,𝑏,𝑐) 𝑈(𝑥,𝑦) 𝑋(𝑥,𝑦,𝑒,𝑓,𝑑) 𝑌(𝑥,𝑦,𝑒,𝑓,𝑎,𝑑) 𝑍(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑑)

**Proof of Theorem xpord3ind**
Step	Hyp	Ref	Expression
1		xpord3.1	. . . . 5 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((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		xpord3ind.1	. . . . . 6 ⊢ 𝑅 Fr 𝐴
3	2	a1i 11	. . . . 5 ⊢ (⊤ → 𝑅 Fr 𝐴)
4		xpord3ind.4	. . . . . 6 ⊢ 𝑆 Fr 𝐵
5	4	a1i 11	. . . . 5 ⊢ (⊤ → 𝑆 Fr 𝐵)
6		xpord3ind.7	. . . . . 6 ⊢ 𝑇 Fr 𝐶
7	6	a1i 11	. . . . 5 ⊢ (⊤ → 𝑇 Fr 𝐶)
8	1, 3, 5, 7	frxp3 33724	. . . 4 ⊢ (⊤ → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
9	8	mptru 1546	. . 3 ⊢ 𝑈 Fr ((𝐴 × 𝐵) × 𝐶)
10		xpord3ind.2	. . . . . 6 ⊢ 𝑅 Po 𝐴
11	10	a1i 11	. . . . 5 ⊢ (⊤ → 𝑅 Po 𝐴)
12		xpord3ind.5	. . . . . 6 ⊢ 𝑆 Po 𝐵
13	12	a1i 11	. . . . 5 ⊢ (⊤ → 𝑆 Po 𝐵)
14		xpord3ind.8	. . . . . 6 ⊢ 𝑇 Po 𝐶
15	14	a1i 11	. . . . 5 ⊢ (⊤ → 𝑇 Po 𝐶)
16	1, 11, 13, 15	poxp3 33723	. . . 4 ⊢ (⊤ → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))
17	16	mptru 1546	. . 3 ⊢ 𝑈 Po ((𝐴 × 𝐵) × 𝐶)
18		xpord3ind.3	. . . . . 6 ⊢ 𝑅 Se 𝐴
19	18	a1i 11	. . . . 5 ⊢ (⊤ → 𝑅 Se 𝐴)
20		xpord3ind.6	. . . . . 6 ⊢ 𝑆 Se 𝐵
21	20	a1i 11	. . . . 5 ⊢ (⊤ → 𝑆 Se 𝐵)
22		xpord3ind.9	. . . . . 6 ⊢ 𝑇 Se 𝐶
23	22	a1i 11	. . . . 5 ⊢ (⊤ → 𝑇 Se 𝐶)
24	1, 19, 21, 23	sexp3 33726	. . . 4 ⊢ (⊤ → 𝑈 Se ((𝐴 × 𝐵) × 𝐶))
25	24	mptru 1546	. . 3 ⊢ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)
26	9, 17, 25	3pm3.2i 1337	. 2 ⊢ (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶))
27	1	xpord3pred 33725	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
28	27	eleq2d 2824	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
29	28	imbi1d 341	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) → 𝜃)))
30		eldifsn 4717	. . . . . . . . . . 11 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
31		ot2elxp 33582	. . . . . . . . . . . 12 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
32		vex 3426	. . . . . . . . . . . . 13 ⊢ 𝑑 ∈ V
33		vex 3426	. . . . . . . . . . . . 13 ⊢ 𝑒 ∈ V
34		vex 3426	. . . . . . . . . . . . 13 ⊢ 𝑓 ∈ V
35	32, 33, 34	otthne 33585	. . . . . . . . . . . 12 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
36	31, 35	anbi12i 626	. . . . . . . . . . 11 ⊢ ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
37	30, 36	bitri 274	. . . . . . . . . 10 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
38	37	imbi1i 349	. . . . . . . . 9 ⊢ ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃))
39		impexp 450	. . . . . . . . 9 ⊢ ((((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
40	38, 39	bitr2i 275	. . . . . . . 8 ⊢ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) → 𝜃))
41	29, 40	bitr4di 288	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
42	41	albidv 1924	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑓(⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
43	42	2albidv 1927	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
44		r3al 3125	. . . . 5 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
45	43, 44	bitr4di 288	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
46		ssun1 4102	. . . . . . . . 9 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
47		ssralv 3983	. . . . . . . . 9 ⊢ (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
48	46, 47	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
49		ssun1 4102	. . . . . . . . . . 11 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
50		ssralv 3983	. . . . . . . . . . 11 ⊢ (Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
51	49, 50	ax-mp 5	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
52		ssun1 4102	. . . . . . . . . . . 12 ⊢ Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
53		ssralv 3983	. . . . . . . . . . . 12 ⊢ (Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
54	52, 53	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
55	54	ralimi 3086	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
56	51, 55	syl 17	. . . . . . . . 9 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
57	56	ralimi 3086	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
58		predpoirr 6225	. . . . . . . . . . . . . . 15 ⊢ (𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
59	14, 58	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)
60		eleq1w 2821	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
61	59, 60	mtbiri 326	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐))
62	61	necon2ai 2972	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → 𝑓 ≠ 𝑐)
63	62	3mix3d 1336	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
64		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
65	63, 64	syl 17	. . . . . . . . . 10 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
66	65	ralimia 3084	. . . . . . . . 9 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
67	66	2ralimi 3087	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
68	48, 57, 67	3syl 18	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
69		ssun2 4103	. . . . . . . . . . . . . 14 ⊢ {𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
70		ssralv 3983	. . . . . . . . . . . . . 14 ⊢ ({𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
71	69, 70	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
72	71	ralimi 3086	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
73	51, 72	syl 17	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
74	73	ralimi 3086	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
75	48, 74	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
76		vex 3426	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
77		biidd 261	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
78		biidd 261	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
79		neeq1 3005	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑓 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
80	77, 78, 79	3orbi123d 1433	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
81		xpord3ind.12	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))
82	81	bicomd 222	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜒))
83	82	equcoms 2024	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (𝜃 ↔ 𝜒))
84	80, 83	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑐 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)))
85	76, 84	ralsn 4614	. . . . . . . . . 10 ⊢ (∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
86	85	2ralbii 3091	. . . . . . . . 9 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
87	75, 86	sylib 217	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
88		predpoirr 6225	. . . . . . . . . . . . . . 15 ⊢ (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
89	12, 88	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)
90		eleq1w 2821	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
91	89, 90	mtbiri 326	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏))
92	91	necon2ai 2972	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑒 ≠ 𝑏)
93	92	3mix2d 1335	. . . . . . . . . . 11 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
94		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
95	93, 94	syl 17	. . . . . . . . . 10 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
96	95	ralimia 3084	. . . . . . . . 9 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
97	96	ralimi 3086	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
98	87, 97	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
99		ssun2 4103	. . . . . . . . . . . . 13 ⊢ {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
100		ssralv 3983	. . . . . . . . . . . . 13 ⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
101	99, 100	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
102	54	ralimi 3086	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
103	101, 102	syl 17	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
104	103	ralimi 3086	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
105	48, 104	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
106		vex 3426	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
107		biidd 261	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
108		neeq1 3005	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑒 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏))
109		biidd 261	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
110	107, 108, 109	3orbi123d 1433	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
111		xpord3ind.15	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))
112		equcom 2022	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 ↔ 𝑒 = 𝑏)
113		bicom 221	. . . . . . . . . . . . . 14 ⊢ ((𝜁 ↔ 𝜃) ↔ (𝜃 ↔ 𝜁))
114	111, 112, 113	3imtr3i 290	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝜃 ↔ 𝜁))
115	110, 114	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
116	115	ralbidv 3120	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
117	106, 116	ralsn 4614	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
118	117	ralbii 3090	. . . . . . . . 9 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
119	105, 118	sylib 217	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
120	62	3mix3d 1336	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
121		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁))
122	120, 121	syl 17	. . . . . . . . . 10 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁))
123	122	ralimia 3084	. . . . . . . . 9 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
124	123	ralimi 3086	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
125	119, 124	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
126	68, 98, 125	3jca 1126	. . . . . 6 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
127	71	ralimi 3086	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
128	101, 127	syl 17	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
129	128	ralimi 3086	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
130	48, 129	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
131	85	ralbii 3090	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
132		biidd 261	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑐 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
133	107, 108, 132	3orbi123d 1433	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
134		xpord3ind.11	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))
135	134	bicomd 222	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝜒 ↔ 𝜓))
136	135	equcoms 2024	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝜒 ↔ 𝜓))
137	133, 136	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)))
138	106, 137	ralsn 4614	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
139	131, 138	bitri 274	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
140	139	ralbii 3090	. . . . . . . . 9 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
141	130, 140	sylib 217	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
142		predpoirr 6225	. . . . . . . . . . . . . 14 ⊢ (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
143	10, 142	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)
144		eleq1w 2821	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
145	143, 144	mtbiri 326	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎))
146	145	necon2ai 2972	. . . . . . . . . . 11 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑑 ≠ 𝑎)
147	146	3mix1d 1334	. . . . . . . . . 10 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
148		pm2.27 42	. . . . . . . . . 10 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
149	147, 148	syl 17	. . . . . . . . 9 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
150	149	ralimia 3084	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
151	141, 150	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
152		ssun2 4103	. . . . . . . . . . 11 ⊢ {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
153		ssralv 3983	. . . . . . . . . . 11 ⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
154	152, 153	ax-mp 5	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
155	56	ralimi 3086	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
156	154, 155	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
157		vex 3426	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
158		neeq1 3005	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑑 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
159		biidd 261	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
160		biidd 261	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
161	158, 159, 160	3orbi123d 1433	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
162		xpord3ind.13	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))
163	162	equcoms 2024	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝜏 ↔ 𝜃))
164	163	bicomd 222	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → (𝜃 ↔ 𝜏))
165	161, 164	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑎 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
166	165	2ralbidv 3122	. . . . . . . . . 10 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
167	157, 166	ralsn 4614	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
168	156, 167	sylib 217	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
169	62	3mix3d 1336	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
170		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏))
171	169, 170	syl 17	. . . . . . . . . 10 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏))
172	171	ralimia 3084	. . . . . . . . 9 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
173	172	ralimi 3086	. . . . . . . 8 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
174	168, 173	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
175	73	ralimi 3086	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
176	154, 175	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
177	165	2ralbidv 3122	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
178	157, 177	ralsn 4614	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
179		biidd 261	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
180	179, 78, 79	3orbi123d 1433	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
181		xpord3ind.16	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))
182	181	bicomd 222	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑓 → (𝜏 ↔ 𝜎))
183	182	equcoms 2024	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝜏 ↔ 𝜎))
184	180, 183	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)))
185	76, 184	ralsn 4614	. . . . . . . . . . 11 ⊢ (∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
186	185	ralbii 3090	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
187	178, 186	bitri 274	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
188	176, 187	sylib 217	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
189	92	3mix2d 1335	. . . . . . . . . 10 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
190		pm2.27 42	. . . . . . . . . 10 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎))
191	189, 190	syl 17	. . . . . . . . 9 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎))
192	191	ralimia 3084	. . . . . . . 8 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)
193	188, 192	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)
194	151, 174, 193	3jca 1126	. . . . . 6 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
195	103	ralimi 3086	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
196	154, 195	syl 17	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
197	165	2ralbidv 3122	. . . . . . . . . 10 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
198	157, 197	ralsn 4614	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
199		biidd 261	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
200	199, 108, 109	3orbi123d 1433	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
201		xpord3ind.14	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))
202	201	equcoms 2024	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝜂 ↔ 𝜏))
203	202	bicomd 222	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → (𝜏 ↔ 𝜂))
204	200, 203	imbi12d 344	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑏 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
205	204	ralbidv 3120	. . . . . . . . . 10 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
206	106, 205	ralsn 4614	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
207	198, 206	bitri 274	. . . . . . . 8 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
208	196, 207	sylib 217	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
209	62	3mix3d 1336	. . . . . . . . 9 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
210		pm2.27 42	. . . . . . . . 9 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂))
211	209, 210	syl 17	. . . . . . . 8 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂))
212	211	ralimia 3084	. . . . . . 7 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)
213	208, 212	syl 17	. . . . . 6 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)
214	126, 194, 213	3jca 1126	. . . . 5 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂))
215		xpord3ind.i	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))
216	214, 215	syl5 34	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜑))
217	45, 216	sylbid 239	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) → 𝜑))
218		xpord3ind.10	. . 3 ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓))
219		xpord3ind.17	. . 3 ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌))
220		xpord3ind.18	. . 3 ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇))
221		xpord3ind.19	. . 3 ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆))
222	217, 218, 134, 81, 219, 220, 221	frpoins3xp3g 33715	. 2 ⊢ (((𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜆)
223	26, 222	mpan 686	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → 𝜆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∨ w3o 1084 ∧ w3a 1085 ∀wal 1537 = wceq 1539 ⊤wtru 1540 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∖ cdif 3880 ∪ cun 3881 ⊆ wss 3883 {csn 4558 ⟨cop 4564 class class class wbr 5070 {copab 5132 Po wpo 5492 Fr wfr 5532 Se wse 5533 × cxp 5578 Predcpred 6190 ‘cfv 6418 1^st c1st 7802 2^nd c2nd 7803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-po 5494 df-fr 5535 df-se 5536 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-iota 6376 df-fun 6420 df-fv 6426 df-1st 7804 df-2nd 7805

This theorem is referenced by: on3ind 33756 no3inds 34042

W3C validator