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 8182

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 3864	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜓))
3	2	sbcbidv 3864	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓))
4	3	cbvsbcvw 3839	. . . . . . 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 3864	. . . . . . . . . 10 ⊢ (𝑦 = 𝑡 → ([(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘𝑞) / 𝑧]𝜒))
7	6	cbvsbcvw 3839	. . . . . . . . 9 ⊢ ([(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜓 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑧]𝜒)
8		frpoins3xp3g.4	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑢 → (𝜒 ↔ 𝜃))
9	8	cbvsbcvw 3839	. . . . . . . . . 10 ⊢ ([(2^nd ‘𝑞) / 𝑧]𝜒 ↔ [(2^nd ‘𝑞) / 𝑢]𝜃)
10	9	sbcbii 3865	. . . . . . . . 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 3865	. . . . . . 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 3099	. . . . 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 8076	. . . . . 6 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩)
16		nfv 1913	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
17		nfsbc1v 3824	. . . . . . . 8 ⊢ Ⅎ𝑥[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
18	16, 17	nfim 1895	. . . . . . 7 ⊢ Ⅎ𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
19		nfv 1913	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
20		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑦∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
21		nfcv 2908	. . . . . . . . . 10 ⊢ Ⅎ𝑦(1^st ‘(1^st ‘𝑝))
22		nfsbc1v 3824	. . . . . . . . . 10 ⊢ Ⅎ𝑦[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
23	21, 22	nfsbcw 3826	. . . . . . . . 9 ⊢ Ⅎ𝑦[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
24	20, 23	nfim 1895	. . . . . . . 8 ⊢ Ⅎ𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
25		nfv 1913	. . . . . . . . . 10 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)
26		nfv 1913	. . . . . . . . . . 11 ⊢ Ⅎ𝑧∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
27		nfcv 2908	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧(1^st ‘(1^st ‘𝑝))
28		nfcv 2908	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧(2^nd ‘(1^st ‘𝑝))
29		nfsbc1v 3824	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑧[(2^nd ‘𝑝) / 𝑧]𝜑
30	28, 29	nfsbcw 3826	. . . . . . . . . . . 12 ⊢ Ⅎ𝑧[(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
31	27, 30	nfsbcw 3826	. . . . . . . . . . 11 ⊢ Ⅎ𝑧[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑
32	26, 31	nfim 1895	. . . . . . . . . 10 ⊢ Ⅎ𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃 → [(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
33		predss 6340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
34		sseqin2 4244	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
35	33, 34	mpbi 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
36	35	eleq2i 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
37	36	bicomi 224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
38		elin 3992	. . . . . . . . . . . . . . . . . . 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 1817	. . . . . . . . . . . . . . 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 3203	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤∀𝑡∀𝑢((𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
46		nfv 1913	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
47		nfsbc1v 3824	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑤[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
48	46, 47	nfim 1895	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
49		nfv 1913	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
50		nfcv 2908	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡(1^st ‘(1^st ‘𝑞))
51		nfsbc1v 3824	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑡[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
52	50, 51	nfsbcw 3826	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑡[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
53	49, 52	nfim 1895	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
54		nfv 1913	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
55		nfcv 2908	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢(1^st ‘(1^st ‘𝑞))
56		nfcv 2908	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢(2^nd ‘(1^st ‘𝑞))
57		nfsbc1v 3824	. . . . . . . . . . . . . . . . . . . 20 ⊢ Ⅎ𝑢[(2^nd ‘𝑞) / 𝑢]𝜃
58	56, 57	nfsbcw 3826	. . . . . . . . . . . . . . . . . . 19 ⊢ Ⅎ𝑢[(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
59	55, 58	nfsbcw 3826	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑢[(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃
60	54, 59	nfim 1895	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃)
61		nfv 1913	. . . . . . . . . . . . . . . . 17 ⊢ Ⅎ𝑞(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)
62		eleq1 2832	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
63		sbcoteq1a 8092	. . . . . . . . . . . . . . . . . 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 8178	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1^st ‘(1^st ‘𝑞)) / 𝑤][(2^nd ‘(1^st ‘𝑞)) / 𝑡][(2^nd ‘𝑞) / 𝑢]𝜃) ↔ ∀𝑤 ∈ 𝐴 ∀𝑡 ∈ 𝐵 ∀𝑢 ∈ 𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
66		elin 3992	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
67	35	eleq2i 2836	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
68		otelxp 5744	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶))
69	68	anbi1i 623	. . . . . . . . . . . . . . . . . . . 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 1819	. . . . . . . . . . . . . . . 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 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 275	. . . . . . . . . . . . . 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	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 6336	. . . . . . . . . . . . . 14 ⊢ (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
83	82	raleqdv 3334	. . . . . . . . . . . . 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 8092	. . . . . . . . . . . . 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 1121	. . . . . . . . . 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 3272	. . . . . . . . 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 3272	. . . . . . 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 3265	. . . . . 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 6925	. . . . 5 ⊢ (𝑝 = 𝑞 → (1^st ‘(1^st ‘𝑝)) = (1^st ‘(1^st ‘𝑞)))
95		2fveq3 6925	. . . . . 6 ⊢ (𝑝 = 𝑞 → (2^nd ‘(1^st ‘𝑝)) = (2^nd ‘(1^st ‘𝑞)))
96		fveq2 6920	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (2^nd ‘𝑝) = (2^nd ‘𝑞))
97	96	sbceq1d 3809	. . . . . 6 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘𝑞) / 𝑧]𝜑))
98	95, 97	sbceqbid 3811	. . . . 5 ⊢ (𝑝 = 𝑞 → ([(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑 ↔ [(2^nd ‘(1^st ‘𝑞)) / 𝑦][(2^nd ‘𝑞) / 𝑧]𝜑))
99	94, 98	sbceqbid 3811	. . . 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 6377	. . 3 ⊢ ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1^st ‘(1^st ‘𝑝)) / 𝑥][(2^nd ‘(1^st ‘𝑝)) / 𝑦][(2^nd ‘𝑝) / 𝑧]𝜑)
101		ralxp3es 8180	. . 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 3651	. 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 1087 ∀wal 1535 = wceq 1537 ∈ wcel 2108 ∀wral 3067 ∃wrex 3076 [wsbc 3804 ∩ cin 3975 ⊆ wss 3976 ⟨cotp 4656 Po wpo 5605 Fr wfr 5649 Se wse 5650 × cxp 5698 Predcpred 6331 ‘cfv 6573 1^st c1st 8028 2^nd c2nd 8029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-ot 4657 df-uni 4932 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-po 5607 df-fr 5652 df-se 5653 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-iota 6525 df-fun 6575 df-fv 6581 df-1st 8030 df-2nd 8031

This theorem is referenced by: xpord3inddlem 8195

W3C validator