frpoins3xp3g - Metamath Proof Explorer

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

Theorem frpoins3xp3g 8123

Description: Special case of founded partial recursion over a triple Cartesian 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 3801	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜓))
3	2	sbcbidv 3801	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓))
4	3	cbvsbcvw 3780	. . . . . . 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 3801	. . . . . . . . . 10 ⊢ (𝑦 = 𝑡 → ([(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘𝑞) / 𝑧]𝜒))
7	6	cbvsbcvw 3780	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒)
8		frpoins3xp3g.4	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃))
9	8	cbvsbcvw 3780	. . . . . . . . . 10 ⊢ ([(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘𝑞) / 𝑢]𝜃)
10	9	sbcbii 3802	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
11	7, 10	bitri 277	. . . . . . . 8 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
12	11	sbcbii 3802	. . . . . . 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 277	. . . . . 6 ⊢ ([(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
14	13	ralbii 3110	. . . . 5 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
15		el2xptp 8018	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩)
16		nfv 1936	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
17		nfsbc1v 3766	. . . . . . . 8 ⊢ Ⅎ𝑥[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
18	16, 17	nfim 1918	. . . . . . 7 ⊢ Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
19		nfv 1936	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
20		nfv 1936	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
21		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑦(1^st ‘(1^st ‘𝑝))
22		nfsbc1v 3766	. . . . . . . . . 10 ⊢ Ⅎ𝑦[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
23	21, 22	nfsbcw 3768	. . . . . . . . 9 ⊢ Ⅎ𝑦[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
24	20, 23	nfim 1918	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
25		nfv 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
26		nfv 1936	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
27		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(1^st ‘(1^st ‘𝑝))
28		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧(2^nd ‘(1^st ‘𝑝))
29		nfsbc1v 3766	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧[(2^nd ‘𝑝) / 𝑧]𝜑
30	28, 29	nfsbcw 3768	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
31	27, 30	nfsbcw 3768	. . . . . . . . . . 11 ⊢ Ⅎ𝑧[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
32	26, 31	nfim 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
33		predss 6298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
34		sseqin2 4177	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
35	33, 34	mpbi 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
36	35	eleq2i 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
37	36	bicomi 226	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
38		elin 3922	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
39	37, 38	bitri 277	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
40	39	imbi1i 351	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
41		impexp 454	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
42	40, 41	bitri 277	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
43	42	albii 1841	. . . . . . . . . . . . . . 15 ⊢ (∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
44	43	bicomi 226	. . . . . . . . . . . . . 14 ⊢ (∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
45		r3al 3202	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
46		nfv 1936	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
47		nfsbc1v 3766	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
48	46, 47	nfim 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
49		nfv 1936	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
50		nfcv 2926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(1^st ‘(1^st ‘𝑞))
51		nfsbc1v 3766	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
52	50, 51	nfsbcw 3768	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
53	49, 52	nfim 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
54		nfv 1936	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
55		nfcv 2926	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢(1^st ‘(1^st ‘𝑞))
56		nfcv 2926	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢(2^nd ‘(1^st ‘𝑞))
57		nfsbc1v 3766	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢[(2^nd ‘𝑞) / 𝑢]𝜃
58	56, 57	nfsbcw 3768	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
59	55, 58	nfsbcw 3768	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
60	54, 59	nfim 1918	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
61		nfv 1936	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑞(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)
62		eleq1 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
63		sbcoteq1a 8034	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ([(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ 𝜃))
64	62, 63	imbi12d 346	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
65	48, 53, 60, 61, 64	ralxp3f 8119	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
66		elin 3922	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
67	35	eleq2i 2856	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
68		otelxp 5693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶))
69	68	anbi1i 633	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
70	66, 67, 69	3bitr3i 303	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
71	70	imbi1i 351	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ (((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃))
72		impexp 454	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
73	71, 72	bitri 277	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
74	73	3albii 1843	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
75	45, 65, 74	3bitr4ri 306	. . . . . . . . . . . . . . 15 ⊢ (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
76		df-ral 3079	. . . . . . . . . . . . . . 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 277	. . . . . . . . . . . . . 14 ⊢ (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
78		df-ral 3079	. . . . . . . . . . . . . 14 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
79	44, 77, 78	3bitr4ri 306	. . . . . . . . . . . . 13 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
80		frpoins3xp3g.1	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) → 𝜑))
81	79, 80	biimtrid 244	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → 𝜑))
82		predeq3 6294	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
83	82	raleqdv 3322	. . . . . . . . . . . . 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 8034	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ 𝜑))
85	83, 84	imbi12d 346	. . . . . . . . . . . 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 249	. . . . . . . . . . 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 1135	. . . . . . . . . 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 3271	. . . . . . . . 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 416	. . . . . . . 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 3271	. . . . . . 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 3264	. . . . . 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 219	. . . . 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	biimtrid 244	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))
94		2fveq3 6874	. . . . 5 ⊢ (𝑝 = 𝑞 → (1^st ‘(1^st ‘𝑝)) = (1^st ‘(1^st ‘𝑞)))
95		2fveq3 6874	. . . . . 6 ⊢ (𝑝 = 𝑞 → (2^nd ‘(1^st ‘𝑝)) = (2^nd ‘(1^st ‘𝑞)))
96		fveq2 6869	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (2^nd ‘𝑝) = (2^nd ‘𝑞))
97	96	sbceq1d 3751	. . . . . 6 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜑))
98	95, 97	sbceqbid 3753	. . . . 5 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑))
99	94, 98	sbceqbid 3753	. . . 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 6334	. . 3 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
101		ralxp3es 8121	. . 3 ⊢ (∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
102	100, 101	sylib 220	. 2 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
103		frpoins3xp3g.5	. . 3 ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏))
104		frpoins3xp3g.6	. . 3 ⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂))
105		frpoins3xp3g.7	. . 3 ⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁))
106	103, 104, 105	rspc3v 3599	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → 𝜁))
107	102, 106	mpan9 514	1 ⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1099 ∀wal 1560 = wceq 1562 ∈ wcel 2144 ∀wral 3078 ∃wrex 3088 [wsbc 3746 ∩ cin 3905 ⊆ wss 3906 ⟨cotp 4592 Po wpo 5555 Fr wfr 5599 Se wse 5600 × cxp 5647 Predcpred 6289 ‘cfv 6523 1^st c1st 7970 2^nd c2nd 7971

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1817 ax-4 1831 ax-5 1932 ax-6 1989 ax-7 2030 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2214 ax-ext 2736 ax-sep 5248 ax-nul 5258 ax-pr 5392 ax-un 7720

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1101 df-tru 1565 df-fal 1575 df-ex 1802 df-nf 1806 df-sb 2093 df-mo 2568 df-eu 2598 df-clab 2743 df-cleq 2756 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3079 df-rex 3089 df-rab 3417 df-v 3458 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-ot 4593 df-uni 4868 df-iun 4953 df-br 5103 df-opab 5165 df-mpt 5184 df-id 5544 df-po 5557 df-fr 5602 df-se 5603 df-xp 5655 df-rel 5656 df-cnv 5657 df-co 5658 df-dm 5659 df-rn 5660 df-res 5661 df-ima 5662 df-pred 6290 df-iota 6479 df-fun 6525 df-fv 6531 df-1st 7972 df-2nd 7973

This theorem is referenced by: xpord3inddlem 8136

W3C validator