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 33367

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 33364	. . . 4 ⊢ (⊤ → 𝑈 Fr ((𝐴 × 𝐵) × 𝐶))
9	8	mptru 1545	. . 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 33363	. . . 4 ⊢ (⊤ → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))
17	16	mptru 1545	. . 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 33366	. . . 4 ⊢ (⊤ → 𝑈 Se ((𝐴 × 𝐵) × 𝐶))
25	24	mptru 1545	. . 3 ⊢ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)
26	9, 17, 25	3pm3.2i 1336	. 2 ⊢ (𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶))
27	1	xpord3pred 33365	. . . . . . . . . 10 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
28	27	eleq2d 2837	. . . . . . . . 9 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
29	28	imbi1d 345	. . . . . . . 8 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) → 𝜃)))
30		eldifsn 4680	. . . . . . . . . . 11 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
31		ot2elxp 33210	. . . . . . . . . . . 12 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
32		vex 3413	. . . . . . . . . . . . 13 ⊢ 𝑑 ∈ V
33		vex 3413	. . . . . . . . . . . . 13 ⊢ 𝑒 ∈ V
34		vex 3413	. . . . . . . . . . . . 13 ⊢ 𝑓 ∈ V
35	32, 33, 34	otthne 33213	. . . . . . . . . . . 12 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
36	31, 35	anbi12i 629	. . . . . . . . . . 11 ⊢ ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
37	30, 36	bitri 278	. . . . . . . . . 10 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
38	37	imbi1i 353	. . . . . . . . 9 ⊢ ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) → 𝜃) ↔ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃))
39		impexp 454	. . . . . . . . 9 ⊢ ((((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
40	38, 39	bitr2i 279	. . . . . . . 8 ⊢ (((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) → 𝜃))
41	29, 40	bitr4di 292	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
42	41	albidv 1921	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑓(⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
43	42	2albidv 1924	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))))
44		r3al 3131	. . . . 5 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑∀𝑒∀𝑓((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
45	43, 44	bitr4di 292	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∀𝑑∀𝑒∀𝑓(⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) → 𝜃) ↔ ∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
46		ssun1 4079	. . . . . . . . 9 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
47		ssralv 3960	. . . . . . . . 9 ⊢ (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
48	46, 47	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
49		ssun1 4079	. . . . . . . . . . 11 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
50		ssralv 3960	. . . . . . . . . . 11 ⊢ (Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
51	49, 50	ax-mp 5	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
52		ssun1 4079	. . . . . . . . . . . 12 ⊢ Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
53		ssralv 3960	. . . . . . . . . . . 12 ⊢ (Pred(𝑇, 𝐶, 𝑐) ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
54	52, 53	ax-mp 5	. . . . . . . . . . 11 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
55	54	ralimi 3092	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
56	51, 55	syl 17	. . . . . . . . 9 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
57	56	ralimi 3092	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
58		predpoirr 6159	. . . . . . . . . . . . . . 15 ⊢ (𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐))
59	14, 58	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)
60		eleq1w 2834	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ 𝑐 ∈ Pred(𝑇, 𝐶, 𝑐)))
61	59, 60	mtbiri 330	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred(𝑇, 𝐶, 𝑐))
62	61	necon2ai 2980	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → 𝑓 ≠ 𝑐)
63	62	3mix3d 1335	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
64		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
65	63, 64	syl 17	. . . . . . . . . 10 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → 𝜃))
66	65	ralimia 3090	. . . . . . . . 9 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
67	66	2ralimi 3093	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
68	48, 57, 67	3syl 18	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃)
69		ssun2 4080	. . . . . . . . . . . . . 14 ⊢ {𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})
70		ssralv 3960	. . . . . . . . . . . . . 14 ⊢ ({𝑐} ⊆ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) → (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
71	69, 70	ax-mp 5	. . . . . . . . . . . . 13 ⊢ (∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
72	71	ralimi 3092	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
73	51, 72	syl 17	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
74	73	ralimi 3092	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
75	48, 74	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
76		vex 3413	. . . . . . . . . . 11 ⊢ 𝑐 ∈ V
77		biidd 265	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
78		biidd 265	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
79		neeq1 3013	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝑓 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
80	77, 78, 79	3orbi123d 1432	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
81		xpord3ind.12	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃))
82	81	bicomd 226	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑓 → (𝜃 ↔ 𝜒))
83	82	equcoms 2027	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (𝜃 ↔ 𝜒))
84	80, 83	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑓 = 𝑐 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒)))
85	76, 84	ralsn 4579	. . . . . . . . . 10 ⊢ (∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
86	85	2ralbii 3098	. . . . . . . . 9 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
87	75, 86	sylib 221	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
88		predpoirr 6159	. . . . . . . . . . . . . . 15 ⊢ (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
89	12, 88	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)
90		eleq1w 2834	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
91	89, 90	mtbiri 330	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred(𝑆, 𝐵, 𝑏))
92	91	necon2ai 2980	. . . . . . . . . . . 12 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑒 ≠ 𝑏)
93	92	3mix2d 1334	. . . . . . . . . . 11 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
94		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
95	93, 94	syl 17	. . . . . . . . . 10 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → 𝜒))
96	95	ralimia 3090	. . . . . . . . 9 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
97	96	ralimi 3092	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
98	87, 97	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
99		ssun2 4080	. . . . . . . . . . . . 13 ⊢ {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
100		ssralv 3960	. . . . . . . . . . . . 13 ⊢ ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
101	99, 100	ax-mp 5	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
102	54	ralimi 3092	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
103	101, 102	syl 17	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
104	103	ralimi 3092	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
105	48, 104	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
106		vex 3413	. . . . . . . . . . 11 ⊢ 𝑏 ∈ V
107		biidd 265	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎))
108		neeq1 3013	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑒 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏))
109		biidd 265	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
110	107, 108, 109	3orbi123d 1432	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
111		xpord3ind.15	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃))
112		equcom 2025	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 ↔ 𝑒 = 𝑏)
113		bicom 225	. . . . . . . . . . . . . 14 ⊢ ((𝜁 ↔ 𝜃) ↔ (𝜃 ↔ 𝜁))
114	111, 112, 113	3imtr3i 294	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝜃 ↔ 𝜁))
115	110, 114	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
116	115	ralbidv 3126	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁)))
117	106, 116	ralsn 4579	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
118	117	ralbii 3097	. . . . . . . . 9 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
119	105, 118	sylib 221	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁))
120	62	3mix3d 1335	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
121		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁))
122	120, 121	syl 17	. . . . . . . . . 10 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → 𝜁))
123	122	ralimia 3090	. . . . . . . . 9 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
124	123	ralimi 3092	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜁) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
125	119, 124	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁)
126	68, 98, 125	3jca 1125	. . . . . 6 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁))
127	71	ralimi 3092	. . . . . . . . . . . 12 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
128	101, 127	syl 17	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
129	128	ralimi 3092	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
130	48, 129	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
131	85	ralbii 3097	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒))
132		biidd 265	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝑏 → (𝑐 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐))
133	107, 108, 132	3orbi123d 1432	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) ↔ (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
134		xpord3ind.11	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒))
135	134	bicomd 226	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝜒 ↔ 𝜓))
136	135	equcoms 2027	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝜒 ↔ 𝜓))
137	133, 136	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓)))
138	106, 137	ralsn 4579	. . . . . . . . . . 11 ⊢ (∀𝑒 ∈ {𝑏} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜒) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
139	131, 138	bitri 278	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
140	139	ralbii 3097	. . . . . . . . 9 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ {𝑏}∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
141	130, 140	sylib 221	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓))
142		predpoirr 6159	. . . . . . . . . . . . . 14 ⊢ (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
143	10, 142	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)
144		eleq1w 2834	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
145	143, 144	mtbiri 330	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred(𝑅, 𝐴, 𝑎))
146	145	necon2ai 2980	. . . . . . . . . . 11 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑑 ≠ 𝑎)
147	146	3mix1d 1333	. . . . . . . . . 10 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → (𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
148		pm2.27 42	. . . . . . . . . 10 ⊢ ((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
149	147, 148	syl 17	. . . . . . . . 9 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) → (((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → 𝜓))
150	149	ralimia 3090	. . . . . . . 8 ⊢ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜓) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
151	141, 150	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
152		ssun2 4080	. . . . . . . . . . 11 ⊢ {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
153		ssralv 3960	. . . . . . . . . . 11 ⊢ ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃)))
154	152, 153	ax-mp 5	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
155	56	ralimi 3092	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
156	154, 155	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
157		vex 3413	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
158		neeq1 3013	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑑 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
159		biidd 265	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏))
160		biidd 265	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐))
161	158, 159, 160	3orbi123d 1432	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
162		xpord3ind.13	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃))
163	162	equcoms 2027	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑎 → (𝜏 ↔ 𝜃))
164	163	bicomd 226	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑎 → (𝜃 ↔ 𝜏))
165	161, 164	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑎 → (((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
166	165	2ralbidv 3128	. . . . . . . . . 10 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
167	157, 166	ralsn 4579	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
168	156, 167	sylib 221	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
169	62	3mix3d 1335	. . . . . . . . . . 11 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
170		pm2.27 42	. . . . . . . . . . 11 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏))
171	169, 170	syl 17	. . . . . . . . . 10 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → 𝜏))
172	171	ralimia 3090	. . . . . . . . 9 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
173	172	ralimi 3092	. . . . . . . 8 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
174	168, 173	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏)
175	73	ralimi 3092	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
176	154, 175	syl 17	. . . . . . . . 9 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
177	165	2ralbidv 3128	. . . . . . . . . . 11 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
178	157, 177	ralsn 4579	. . . . . . . . . 10 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
179		biidd 265	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑐 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
180	179, 78, 79	3orbi123d 1432	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
181		xpord3ind.16	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏))
182	181	bicomd 226	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑓 → (𝜏 ↔ 𝜎))
183	182	equcoms 2027	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑐 → (𝜏 ↔ 𝜎))
184	180, 183	imbi12d 348	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝑐 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎)))
185	76, 184	ralsn 4579	. . . . . . . . . . 11 ⊢ (∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
186	185	ralbii 3097	. . . . . . . . . 10 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
187	178, 186	bitri 278	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ {𝑐} ((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
188	176, 187	sylib 221	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎))
189	92	3mix2d 1334	. . . . . . . . . 10 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
190		pm2.27 42	. . . . . . . . . 10 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎))
191	189, 190	syl 17	. . . . . . . . 9 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → 𝜎))
192	191	ralimia 3090	. . . . . . . 8 ⊢ (∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐) → 𝜎) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)
193	188, 192	syl 17	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎)
194	151, 174, 193	3jca 1125	. . . . . 6 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎))
195	103	ralimi 3092	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
196	154, 195	syl 17	. . . . . . . 8 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃))
197	165	2ralbidv 3128	. . . . . . . . . 10 ⊢ (𝑑 = 𝑎 → (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏)))
198	157, 197	ralsn 4579	. . . . . . . . 9 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏))
199		biidd 265	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎))
200	199, 108, 109	3orbi123d 1432	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → ((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) ↔ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
201		xpord3ind.14	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏))
202	201	equcoms 2027	. . . . . . . . . . . . 13 ⊢ (𝑒 = 𝑏 → (𝜂 ↔ 𝜏))
203	202	bicomd 226	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝑏 → (𝜏 ↔ 𝜂))
204	200, 203	imbi12d 348	. . . . . . . . . . 11 ⊢ (𝑒 = 𝑏 → (((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
205	204	ralbidv 3126	. . . . . . . . . 10 ⊢ (𝑒 = 𝑏 → (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂)))
206	106, 205	ralsn 4579	. . . . . . . . 9 ⊢ (∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜏) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
207	198, 206	bitri 278	. . . . . . . 8 ⊢ (∀𝑑 ∈ {𝑎}∀𝑒 ∈ {𝑏}∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) ↔ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
208	196, 207	sylib 221	. . . . . . 7 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂))
209	62	3mix3d 1335	. . . . . . . . 9 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
210		pm2.27 42	. . . . . . . . 9 ⊢ ((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂))
211	209, 210	syl 17	. . . . . . . 8 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) → (((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → 𝜂))
212	211	ralimia 3090	. . . . . . 7 ⊢ (∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)((𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜂) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)
213	208, 212	syl 17	. . . . . 6 ⊢ (∀𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})∀𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})((𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐) → 𝜃) → ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂)
214	126, 194, 213	3jca 1125	. . . . 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 243	. . 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 33345	. 2 ⊢ (((𝑈 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑈 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜆)
223	26, 222	mpan 689	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → 𝜆)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∨ w3o 1083 ∧ w3a 1084 ∀wal 1536 = wceq 1538 ⊤wtru 1539 ∈ wcel 2111 ≠ wne 2951 ∀wral 3070 ∖ cdif 3857 ∪ cun 3858 ⊆ wss 3860 {csn 4525 ⟨cop 4531 class class class wbr 5036 {copab 5098 Po wpo 5445 Fr wfr 5484 Se wse 5485 × cxp 5526 Predcpred 6130 ‘cfv 6340 1^st c1st 7697 2^nd c2nd 7698

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4802 df-iun 4888 df-br 5037 df-opab 5099 df-mpt 5117 df-id 5434 df-po 5447 df-fr 5487 df-se 5488 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-iota 6299 df-fun 6342 df-fv 6348 df-1st 7699 df-2nd 7700

This theorem is referenced by: on3ind 33426

W3C validator