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 33391

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 3736	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜓))
3	2	sbcbidv 3736	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓))
4	3	cbvsbcvw 3715	. . . . . . 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 3736	. . . . . . . . . 10 ⊢ (𝑦 = 𝑡 → ([(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘𝑞) / 𝑧]𝜒))
7	6	cbvsbcvw 3715	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒)
8		frpoins3xp3g.4	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃))
9	8	cbvsbcvw 3715	. . . . . . . . . 10 ⊢ ([(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘𝑞) / 𝑢]𝜃)
10	9	sbcbii 3738	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
11	7, 10	bitri 278	. . . . . . . 8 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
12	11	sbcbii 3738	. . . . . . 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 278	. . . . . 6 ⊢ ([(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
14	13	ralbii 3080	. . . . 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 33257	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
16		nfv 1921	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
17		nfsbc1v 3700	. . . . . . . 8 ⊢ Ⅎ𝑥[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
18	16, 17	nfim 1903	. . . . . . 7 ⊢ Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
19		nfv 1921	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
20		nfv 1921	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
21		nfcv 2899	. . . . . . . . . 10 ⊢ Ⅎ𝑦(1^st ‘(1^st ‘𝑝))
22		nfsbc1v 3700	. . . . . . . . . 10 ⊢ Ⅎ𝑦[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
23	21, 22	nfsbcw 3702	. . . . . . . . 9 ⊢ Ⅎ𝑦[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
24	20, 23	nfim 1903	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
25		nfv 1921	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
26		nfv 1921	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
27		nfcv 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(1^st ‘(1^st ‘𝑝))
28		nfcv 2899	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧(2^nd ‘(1^st ‘𝑝))
29		nfsbc1v 3700	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧[(2^nd ‘𝑝) / 𝑧]𝜑
30	28, 29	nfsbcw 3702	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
31	27, 30	nfsbcw 3702	. . . . . . . . . . 11 ⊢ Ⅎ𝑧[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
32	26, 31	nfim 1903	. . . . . . . . . 10 ⊢ Ⅎ𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
33		impexp 454	. . . . . . . . . . . . . . . 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 3859	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
35		predss 6136	. . . . . . . . . . . . . . . . . . . 20 ⊢ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
36		sseqin2 4106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
37	35, 36	mpbi 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
38	37	eleq2i 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
39	34, 38	bitr3i 280	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
40	39	imbi1i 353	. . . . . . . . . . . . . . . 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 280	. . . . . . . . . . . . . . 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 1826	. . . . . . . . . . . . . 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 3114	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
44		nfv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
45		nfsbc1v 3700	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
46	44, 45	nfim 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
47		nfv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
48		nfcv 2899	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(1^st ‘(1^st ‘𝑞))
49		nfsbc1v 3700	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
50	48, 49	nfsbcw 3702	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
51	47, 50	nfim 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
52		nfv 1921	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
53		nfcv 2899	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢(1^st ‘(1^st ‘𝑞))
54		nfcv 2899	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢(2^nd ‘(1^st ‘𝑞))
55		nfsbc1v 3700	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢[(2^nd ‘𝑞) / 𝑢]𝜃
56	54, 55	nfsbcw 3702	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
57	53, 56	nfsbcw 3702	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
58	52, 57	nfim 1903	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
59		nfv 1921	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑞(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)
60		eleq1 2820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
61		sbcoteq1a 33261	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → ([(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ 𝜃))
62	60, 61	imbi12d 348	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
63	46, 51, 58, 59, 62	ralxp3f 33259	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
64		elin 3859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
65	37	eleq2i 2824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
66	64, 65	bitr3i 280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
67	66	imbi1i 353	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
68		impexp 454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
69	67, 68	bitr3i 280	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
70		ot2elxp 33253	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶))
71	70	imbi1i 353	. . . . . . . . . . . . . . . . . . 19 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
72	69, 71	bitri 278	. . . . . . . . . . . . . . . . . 18 ⊢ ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
73	72	albii 1826	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
74	73	2albii 1827	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
75	43, 63, 74	3bitr4ri 307	. . . . . . . . . . . . . . 15 ⊢ (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃))
76		df-ral 3058	. . . . . . . . . . . . . . 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 278	. . . . . . . . . . . . . 14 ⊢ (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)))
78		df-ral 3058	. . . . . . . . . . . . . 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 307	. . . . . . . . . . . . 13 ⊢ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 ↔ ∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
80		frpoins3xp3g.1	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑤∀𝑡∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) → 𝜑))
81	79, 80	syl5bi 245	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → 𝜑))
82		predeq3 6133	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
83	82	raleqdv 3316	. . . . . . . . . . . . 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 33261	. . . . . . . . . . . . 13 ⊢ (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ([(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ 𝜑))
85	83, 84	imbi12d 348	. . . . . . . . . . . 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 250	. . . . . . . . . . 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 1122	. . . . . . . . . 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 3227	. . . . . . . . 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 3227	. . . . . . 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 3225	. . . . . 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 220	. . . . 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 245	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑥][(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑))
94		2fveq3 6679	. . . . 5 ⊢ (𝑝 = 𝑞 → (1^st ‘(1^st ‘𝑝)) = (1^st ‘(1^st ‘𝑞)))
95		2fveq3 6679	. . . . . 6 ⊢ (𝑝 = 𝑞 → (2^nd ‘(1^st ‘𝑝)) = (2^nd ‘(1^st ‘𝑞)))
96		fveq2 6674	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (2^nd ‘𝑝) = (2^nd ‘𝑞))
97	96	sbceq1d 3685	. . . . . 6 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜑))
98	95, 97	sbceqbid 3687	. . . . 5 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑))
99	94, 98	sbceqbid 3687	. . . 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 33388	. . 3 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
101		ralxp3es 33262	. . 3 ⊢ (∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
102	100, 101	sylib 221	. 2 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑)
103		frpoins3xp3g.5	. . 3 ⊢ (𝑥 = 𝑋 → (𝜑 ↔ 𝜏))
104		frpoins3xp3g.6	. . 3 ⊢ (𝑦 = 𝑌 → (𝜏 ↔ 𝜂))
105		frpoins3xp3g.7	. . 3 ⊢ (𝑧 = 𝑍 → (𝜂 ↔ 𝜁))
106	103, 104, 105	rspc3v 3539	. 2 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐶 𝜑 → 𝜁))
107	102, 106	mpan9 510	1 ⊢ (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶)) → 𝜁)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 ∀wal 1540 = wceq 1542 ∈ wcel 2114 ∀wral 3053 ∃wrex 3054 [wsbc 3680 ∩ cin 3842 ⊆ wss 3843 ⟨cop 4522 Po wpo 5440 Fr wfr 5480 Se wse 5481 × cxp 5523 Predcpred 6128 ‘cfv 6339 1^st c1st 7712 2^nd c2nd 7713

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 ax-un 7479

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-uni 4797 df-iun 4883 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5429 df-po 5442 df-fr 5483 df-se 5484 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-iota 6297 df-fun 6341 df-fv 6347 df-1st 7714 df-2nd 7715

This theorem is referenced by: xpord3ind 33413

W3C validator