frpoins3xp3g - Mathbox for Scott Fenton

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

Theorem frpoins3xp3g 33715

Description: Special case of founded partial recursion over a triple cross product. (Contributed by Scott Fenton, 22-Aug-2024.)

**Hypotheses**
Ref	Expression
frpoins3xp3g.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) → 𝜑))
frpoins3xp3g.2	⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))
frpoins3xp3g.3	⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))
frpoins3xp3g.4	⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃))
frpoins3xp3g.5	⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏))
frpoins3xp3g.6	⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂))
frpoins3xp3g.7	⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁))

**Assertion**
Ref	Expression
frpoins3xp3g	⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁)

Distinct variable groups: 𝑥,𝐴,𝑦,𝑧 𝑥,𝐵,𝑦,𝑧 𝑥,𝐶,𝑦,𝑧 𝜂,𝑦 𝜏,𝑥 𝑥,𝑋,𝑦,𝑧 𝑦,𝑌,𝑧 𝑧,𝑍 𝜁,𝑧 𝑡,𝐴,𝑢,𝑤 𝑡,𝐵,𝑢,𝑤 𝑡,𝐶,𝑢,𝑤 𝜒,𝑢,𝑦 𝜑,𝑤 𝜓,𝑡,𝑥 𝑡,𝑅,𝑢,𝑤,𝑥,𝑦,𝑧 𝜃,𝑥,𝑦,𝑧 𝑤,𝑢,𝑥,𝑦,𝑧 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑧,𝑢,𝑡) 𝜓(𝑦,𝑧,𝑤,𝑢) 𝜒(𝑥,𝑧,𝑤,𝑡) 𝜃(𝑤,𝑢,𝑡) 𝜏(𝑦,𝑧,𝑤,𝑢,𝑡) 𝜂(𝑥,𝑧,𝑤,𝑢,𝑡) 𝜁(𝑥,𝑦,𝑤,𝑢,𝑡) 𝑋(𝑤,𝑢,𝑡) 𝑌(𝑥,𝑤,𝑢,𝑡) 𝑍(𝑥,𝑦,𝑤,𝑢,𝑡)

Proof of Theorem frpoins3xp3g Dummy variables 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		frpoins3xp3g.2	. . . . . . . . . 10 ⊢ (𝑥 = 𝑤 → (𝜑 ↔ 𝜓))
2	1	sbcbidv 3770	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜓))
3	2	sbcbidv 3770	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓))
4	3	cbvsbcvw 3746	. . . . . . 7 ⊢ ([(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓)
5		frpoins3xp3g.3	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑡 → (𝜓 ↔ 𝜒))
6	5	sbcbidv 3770	. . . . . . . . . 10 ⊢ (𝑦 = 𝑡 → ([(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘𝑞) / 𝑧]𝜒))
7	6	cbvsbcvw 3746	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒)
8		frpoins3xp3g.4	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃))
9	8	cbvsbcvw 3746	. . . . . . . . . 10 ⊢ ([(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘𝑞) / 𝑢]𝜃)
10	9	sbcbii 3772	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
11	7, 10	bitri 274	. . . . . . . 8 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
12	11	sbcbii 3772	. . . . . . 7 ⊢ ([(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
13	4, 12	bitri 274	. . . . . 6 ⊢ ([(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
14	13	ralbii 3090	. . . . 5 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
15		elxpxp 33586	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
16		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
17		nfsbc1v 3731	. . . . . . . 8 ⊢ Ⅎ𝑥[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
18	16, 17	nfim 1900	. . . . . . 7 ⊢ Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
19		nfv 1918	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
20		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
21		nfcv 2906	. . . . . . . . . 10 ⊢ Ⅎ𝑦(1^st ‘(1^st ‘𝑝))
22		nfsbc1v 3731	. . . . . . . . . 10 ⊢ Ⅎ𝑦[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
23	21, 22	nfsbcw 3733	. . . . . . . . 9 ⊢ Ⅎ𝑦[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
24	20, 23	nfim 1900	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
25		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
26		nfv 1918	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
27		nfcv 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(1^st ‘(1^st ‘𝑝))
28		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧(2^nd ‘(1^st ‘𝑝))
29		nfsbc1v 3731	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧[(2^nd ‘𝑝) / 𝑧]𝜑
30	28, 29	nfsbcw 3733	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
31	27, 30	nfsbcw 3733	. . . . . . . . . . 11 ⊢ Ⅎ𝑧[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
32	26, 31	nfim 1900	. . . . . . . . . 10 ⊢ Ⅎ𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
33		impexp 450	. . . . . . . . . . . . . . . 16 ⊢ (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
34		elin 3899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
35		predss 6199	. . . . . . . . . . . . . . . . . . . 20 ⊢ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
36		sseqin2 4146	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
37	35, 36	mpbi 229	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
38	37	eleq2i 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
39	34, 38	bitr3i 276	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
40	39	imbi1i 349	. . . . . . . . . . . . . . . 16 ⊢ (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
41	33, 40	bitr3i 276	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)) ↔ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
42	41	albii 1823	. . . . . . . . . . . . . 14 ⊢ (∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
43		r3al 3125	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
44		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
45		nfsbc1v 3731	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
46	44, 45	nfim 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
47		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
48		nfcv 2906	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(1^st ‘(1^st ‘𝑞))
49		nfsbc1v 3731	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
50	48, 49	nfsbcw 3733	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
51	47, 50	nfim 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
52		nfv 1918	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
53		nfcv 2906	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢(1^st ‘(1^st ‘𝑞))
54		nfcv 2906	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢(2^nd ‘(1^st ‘𝑞))
55		nfsbc1v 3731	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢[(2^nd ‘𝑞) / 𝑢]𝜃
56	54, 55	nfsbcw 3733	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
57	53, 56	nfsbcw 3733	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
58	52, 57	nfim 1900	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
59		nfv 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑞(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)
60		eleq1 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
61		sbcoteq1a 33590	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → ([(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ 𝜃))
62	60, 61	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
63	46, 51, 58, 59, 62	ralxp3f 33588	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
64		elin 3899	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
65	37	eleq2i 2830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
66	64, 65	bitr3i 276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
67	66	imbi1i 349	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
68		impexp 450	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
69	67, 68	bitr3i 276	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
70		ot2elxp 33582	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶))
71	70	imbi1i 349	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
72	69, 71	bitri 274	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
73	72	albii 1823	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
74	73	2albii 1824	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
75	43, 63, 74	3bitr4ri 303	. . . . . . . . . . . . . . 15 ⊢ (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
76		df-ral 3068	. . . . . . . . . . . . . . 15 ⊢ (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
77	75, 76	bitri 274	. . . . . . . . . . . . . 14 ⊢ (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
78		df-ral 3068	. . . . . . . . . . . . . 14 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
79	42, 77, 78	3bitr4ri 303	. . . . . . . . . . . . 13 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
80		frpoins3xp3g.1	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) → 𝜑))
81	79, 80	syl5bi 241	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → 𝜑))
82		predeq3 6195	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
83	82	raleqdv 3339	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
84		sbcoteq1a 33590	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ([(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ 𝜑))
85	83, 84	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ((∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑) ↔ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → 𝜑)))
86	81, 85	syl5ibrcom 246	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)))
87	86	3expia 1119	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ 𝐶 → (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))))
88	25, 32, 87	rexlimd 3245	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (∃𝑧 ∈ 𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)))
89	88	ex 412	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (∃𝑧 ∈ 𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))))
90	19, 24, 89	rexlimd 3245	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)))
91	18, 90	rexlimi 3243	. . . . . 6 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))
92	15, 91	sylbi 216	. . . . 5 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))
93	14, 92	syl5bi 241	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))
94		2fveq3 6761	. . . . 5 ⊢ (𝑝 = 𝑞 → (1^st ‘(1^st ‘𝑝)) = (1^st ‘(1^st ‘𝑞)))
95		2fveq3 6761	. . . . . 6 ⊢ (𝑝 = 𝑞 → (2^nd ‘(1^st ‘𝑝)) = (2^nd ‘(1^st ‘𝑞)))
96		fveq2 6756	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (2^nd ‘𝑝) = (2^nd ‘𝑞))
97	96	sbceq1d 3716	. . . . . 6 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜑))
98	95, 97	sbceqbid 3718	. . . . 5 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑))
99	94, 98	sbceqbid 3718	. . . 4 ⊢ (𝑝 = 𝑞 → ([(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑))
100	93, 99	frpoins2g 6233	. . 3 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
101		ralxp3es 33591	. . 3 ⊢ (∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
102	100, 101	sylib 217	. 2 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
103		frpoins3xp3g.5	. . 3 ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏))
104		frpoins3xp3g.6	. . 3 ⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂))
105		frpoins3xp3g.7	. . 3 ⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁))
106	103, 104, 105	rspc3v 3565	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → 𝜁))
107	102, 106	mpan9 506	1 ⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 ∀wal 1537 = wceq 1539 ∈ wcel 2108 ∀wral 3063 ∃wrex 3064 [wsbc 3711 ∩ cin 3882 ⊆ wss 3883 ⟨cop 4564 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-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 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: xpord3ind 33727

W3C validator