xpord3pred - Metamath Proof Explorer

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

Theorem xpord3pred 8143

Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025.)

**Hypothesis**
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 ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}

**Assertion**
Ref	Expression
xpord3pred	⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 𝑥,𝑅,𝑦 𝑥,𝑆,𝑦 𝑥,𝑇,𝑦 Allowed substitution hints: 𝑈(𝑥,𝑦) 𝑋(𝑥,𝑦) 𝑌(𝑥,𝑦) 𝑍(𝑥,𝑦)

Proof of Theorem xpord3pred Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oteq1 4882	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩)
2		predeq3 6304	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
4		predeq3 6304	. . . . . . 7 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4638	. . . . . . 7 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4164	. . . . . 6 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5705	. . . . 5 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	7	xpeq1d 5705	. . . 4 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
9	1	sneqd 4640	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑏, 𝑐⟩})
10	8, 9	difeq12d 4123	. . 3 ⊢ (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}))
11	3, 10	eqeq12d 2747	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩})))
12		oteq2 4883	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩)
13		predeq3 6304	. . . 4 ⊢ (⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
14	12, 13	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
15		predeq3 6304	. . . . . . 7 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
16		sneq 4638	. . . . . . 7 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
17	15, 16	uneq12d 4164	. . . . . 6 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
18	17	xpeq2d 5706	. . . . 5 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
19	18	xpeq1d 5705	. . . 4 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
20	12	sneqd 4640	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑐⟩})
21	19, 20	difeq12d 4123	. . 3 ⊢ (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}))
22	14, 21	eqeq12d 2747	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩})))
23		oteq3 4884	. . . 4 ⊢ (𝑐 = 𝑍 → ⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩)
24		predeq3 6304	. . . 4 ⊢ (⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
25	23, 24	syl 17	. . 3 ⊢ (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
26		predeq3 6304	. . . . . 6 ⊢ (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
27		sneq 4638	. . . . . 6 ⊢ (𝑐 = 𝑍 → {𝑐} = {𝑍})
28	26, 27	uneq12d 4164	. . . . 5 ⊢ (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
29	28	xpeq2d 5706	. . . 4 ⊢ (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
30	23	sneqd 4640	. . . 4 ⊢ (𝑐 = 𝑍 → {⟨𝑋, 𝑌, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑍⟩})
31	29, 30	difeq12d 4123	. . 3 ⊢ (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
32	25, 31	eqeq12d 2747	. 2 ⊢ (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩})))
33		el2xptp 8025	. . . . . . 7 ⊢ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
34		df-3an 1088	. . . . . . . . . . 11 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
35		simplrl 774	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑑 ∈ 𝐴)
36		simplrr 775	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑒 ∈ 𝐵)
37		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ 𝐶)
38	35, 36, 37	3jca 1127	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
39		simpll 764	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
40	38, 39	jca 511	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
41	40	biantrurd 532	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
42	35	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑𝑅𝑎 ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)))
43	42	orbi1d 914	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
44	36	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑒𝑆𝑏 ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)))
45	44	orbi1d 914	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
46	37	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑓𝑇𝑐 ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)))
47	46	orbi1d 914	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑓𝑇𝑐 ∨ 𝑓 = 𝑐) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
48	43, 45, 47	3anbi123d 1435	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
49	48	anbi1d 629	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
50	41, 49	bitr3d 281	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
51	34, 50	bitrid 283	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
52		breq1 5151	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑎, 𝑏, 𝑐⟩))
53		xpord3.1	. . . . . . . . . . . . 13 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((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 ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
54	53	xpord3lem 8140	. . . . . . . . . . . 12 ⊢ (⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
55	52, 54	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
56		eleq1 2820	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
57		eldifsn 4790	. . . . . . . . . . . . 13 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
58		otelxp 5720	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
59		elun 4148	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
60		vex 3477	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
61	60	elpred 6317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)))
62	61	elv 3479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎))
63		velsn 4644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
64	62, 63	orbi12i 912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
65	59, 64	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
66		elun 4148	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
67		vex 3477	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
68	67	elpred 6317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)))
69	68	elv 3479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏))
70		velsn 4644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
71	69, 70	orbi12i 912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
72	66, 71	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
73		elun 4148	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
74		vex 3477	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
75	74	elpred 6317	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)))
76	75	elv 3479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐))
77		velsn 4644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
78	76, 77	orbi12i 912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
79	73, 78	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
80	65, 72, 79	3anbi123i 1154	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
81	58, 80	bitri 275	. . . . . . . . . . . . . 14 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
82	60, 67, 74	otthne 5486	. . . . . . . . . . . . . 14 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
83	81, 82	anbi12i 626	. . . . . . . . . . . . 13 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
84	57, 83	bitri 275	. . . . . . . . . . . 12 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
85	56, 84	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
86	55, 85	bibi12d 345	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
87	51, 86	syl5ibrcom 246	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
88	87	rexlimdva 3154	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) → (∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
89	88	rexlimdvva 3210	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
90	33, 89	biimtrid 241	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
91	90	pm5.32d 576	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
92		otex 5465	. . . . . 6 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
93		vex 3477	. . . . . . 7 ⊢ 𝑞 ∈ V
94	93	elpred 6317	. . . . . 6 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩)))
95	92, 94	ax-mp 5	. . . . 5 ⊢ (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
96		elin 3964	. . . . 5 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
97	91, 95, 96	3bitr4g 314	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
98	97	eqrdv 2729	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
99		predss 6308	. . . . . . . . . 10 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
100	99	a1i 11	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
101		snssi 4811	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
102	100, 101	unssd 4186	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
103	102	3ad2ant1 1132	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
104		predss 6308	. . . . . . . . . 10 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
105	104	a1i 11	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
106		snssi 4811	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
107	105, 106	unssd 4186	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
108	107	3ad2ant2 1133	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
109		xpss12 5691	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
110	103, 108, 109	syl2anc 583	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
111		predss 6308	. . . . . . . . 9 ⊢ Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
112	111	a1i 11	. . . . . . . 8 ⊢ (𝑐 ∈ 𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
113		snssi 4811	. . . . . . . 8 ⊢ (𝑐 ∈ 𝐶 → {𝑐} ⊆ 𝐶)
114	112, 113	unssd 4186	. . . . . . 7 ⊢ (𝑐 ∈ 𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
115	114	3ad2ant3 1134	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
116		xpss12 5691	. . . . . 6 ⊢ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
117	110, 115, 116	syl2anc 583	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
118	117	ssdifssd 4142	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
119		sseqin2 4215	. . . 4 ⊢ (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
120	118, 119	sylib 217	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
121	98, 120	eqtrd 2771	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
122	11, 22, 32, 121	vtocl3ga 3570	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 844 ∨ w3o 1085 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ∃wrex 3069 Vcvv 3473 ∖ cdif 3945 ∪ cun 3946 ∩ cin 3947 ⊆ wss 3948 {csn 4628 ⟨cotp 4636 class class class wbr 5148 {copab 5210 × cxp 5674 Predcpred 6299 ‘cfv 6543 1^st c1st 7977 2^nd c2nd 7978

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 ax-un 7729

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-ot 4637 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-iota 6495 df-fun 6545 df-fv 6551 df-1st 7979 df-2nd 7980

This theorem is referenced by: sexp3 8144 xpord3inddlem 8145

W3C validator