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 8165

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 3851	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜓))
3	2	sbcbidv 3851	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓))
4	3	cbvsbcvw 3826	. . . . . . 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 3851	. . . . . . . . . 10 ⊢ (𝑦 = 𝑡 → ([(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘𝑞) / 𝑧]𝜒))
7	6	cbvsbcvw 3826	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒)
8		frpoins3xp3g.4	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃))
9	8	cbvsbcvw 3826	. . . . . . . . . 10 ⊢ ([(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘𝑞) / 𝑢]𝜃)
10	9	sbcbii 3852	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
11	7, 10	bitri 275	. . . . . . . 8 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
12	11	sbcbii 3852	. . . . . . 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 275	. . . . . 6 ⊢ ([(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
14	13	ralbii 3091	. . . . 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 8059	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩)
16		nfv 1912	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
17		nfsbc1v 3811	. . . . . . . 8 ⊢ Ⅎ𝑥[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
18	16, 17	nfim 1894	. . . . . . 7 ⊢ Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
19		nfv 1912	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
20		nfv 1912	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
21		nfcv 2903	. . . . . . . . . 10 ⊢ Ⅎ𝑦(1^st ‘(1^st ‘𝑝))
22		nfsbc1v 3811	. . . . . . . . . 10 ⊢ Ⅎ𝑦[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
23	21, 22	nfsbcw 3813	. . . . . . . . 9 ⊢ Ⅎ𝑦[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
24	20, 23	nfim 1894	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
25		nfv 1912	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
26		nfv 1912	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
27		nfcv 2903	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(1^st ‘(1^st ‘𝑝))
28		nfcv 2903	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧(2^nd ‘(1^st ‘𝑝))
29		nfsbc1v 3811	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧[(2^nd ‘𝑝) / 𝑧]𝜑
30	28, 29	nfsbcw 3813	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
31	27, 30	nfsbcw 3813	. . . . . . . . . . 11 ⊢ Ⅎ𝑧[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
32	26, 31	nfim 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
33		predss 6331	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
34		sseqin2 4231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
35	33, 34	mpbi 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
36	35	eleq2i 2831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
37	36	bicomi 224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
38		elin 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
39	37, 38	bitri 275	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
40	39	imbi1i 349	. . . . . . . . . . . . . . . . 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 450	. . . . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . . . . 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 1816	. . . . . . . . . . . . . . 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 224	. . . . . . . . . . . . . 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 3195	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
46		nfv 1912	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
47		nfsbc1v 3811	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
48	46, 47	nfim 1894	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
49		nfv 1912	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
50		nfcv 2903	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(1^st ‘(1^st ‘𝑞))
51		nfsbc1v 3811	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
52	50, 51	nfsbcw 3813	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
53	49, 52	nfim 1894	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
54		nfv 1912	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
55		nfcv 2903	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢(1^st ‘(1^st ‘𝑞))
56		nfcv 2903	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢(2^nd ‘(1^st ‘𝑞))
57		nfsbc1v 3811	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢[(2^nd ‘𝑞) / 𝑢]𝜃
58	56, 57	nfsbcw 3813	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
59	55, 58	nfsbcw 3813	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
60	54, 59	nfim 1894	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
61		nfv 1912	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑞(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)
62		eleq1 2827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
63		sbcoteq1a 8075	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ([(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ 𝜃))
64	62, 63	imbi12d 344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
65	48, 53, 60, 61, 64	ralxp3f 8161	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
66		elin 3979	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
67	35	eleq2i 2831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
68		otelxp 5733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶))
69	68	anbi1i 624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
70	66, 67, 69	3bitr3i 301	. . . . . . . . . . . . . . . . . . 19 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
71	70	imbi1i 349	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ (((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃))
72		impexp 450	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
73	71, 72	bitri 275	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
74	73	3albii 1818	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
75	45, 65, 74	3bitr4ri 304	. . . . . . . . . . . . . . 15 ⊢ (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
76		df-ral 3060	. . . . . . . . . . . . . . 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 275	. . . . . . . . . . . . . 14 ⊢ (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
78		df-ral 3060	. . . . . . . . . . . . . 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 304	. . . . . . . . . . . . 13 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
80		frpoins3xp3g.1	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) → 𝜑))
81	79, 80	biimtrid 242	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → 𝜑))
82		predeq3 6327	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
83	82	raleqdv 3324	. . . . . . . . . . . . 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 8075	. . . . . . . . . . . . 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 247	. . . . . . . . . . 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 1120	. . . . . . . . . 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 3264	. . . . . . . . 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 3264	. . . . . . 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 3257	. . . . . 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 217	. . . . 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 242	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))
94		2fveq3 6912	. . . . 5 ⊢ (𝑝 = 𝑞 → (1^st ‘(1^st ‘𝑝)) = (1^st ‘(1^st ‘𝑞)))
95		2fveq3 6912	. . . . . 6 ⊢ (𝑝 = 𝑞 → (2^nd ‘(1^st ‘𝑝)) = (2^nd ‘(1^st ‘𝑞)))
96		fveq2 6907	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (2^nd ‘𝑝) = (2^nd ‘𝑞))
97	96	sbceq1d 3796	. . . . . 6 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜑))
98	95, 97	sbceqbid 3798	. . . . 5 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑))
99	94, 98	sbceqbid 3798	. . . 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 6368	. . 3 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
101		ralxp3es 8163	. . 3 ⊢ (∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
102	100, 101	sylib 218	. 2 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
103		frpoins3xp3g.5	. . 3 ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏))
104		frpoins3xp3g.6	. . 3 ⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂))
105		frpoins3xp3g.7	. . 3 ⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁))
106	103, 104, 105	rspc3v 3638	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → 𝜁))
107	102, 106	mpan9 506	1 ⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1535 = wceq 1537 ∈ wcel 2106 ∀wral 3059 ∃wrex 3068 [wsbc 3791 ∩ cin 3962 ⊆ wss 3963 ⟨cotp 4639 Po wpo 5595 Fr wfr 5638 Se wse 5639 × cxp 5687 Predcpred 6322 ‘cfv 6563 1^st c1st 8011 2^nd c2nd 8012

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 ax-un 7754

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-ot 4640 df-uni 4913 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5583 df-po 5597 df-fr 5641 df-se 5642 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-iota 6516 df-fun 6565 df-fv 6571 df-1st 8013 df-2nd 8014

This theorem is referenced by: xpord3inddlem 8178

W3C validator