frpoins3xp3g

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

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

Proof

Step	Hyp	Ref	Expression
1		frpoins3xp3g.1	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) → 𝜑 ) )
2		frpoins3xp3g.2	⊢ ( 𝑥 = 𝑤 → ( 𝜑 ↔ 𝜓 ) )
3		frpoins3xp3g.3	⊢ ( 𝑦 = 𝑡 → ( 𝜓 ↔ 𝜒 ) )
4		frpoins3xp3g.4	⊢ ( 𝑧 = 𝑢 → ( 𝜒 ↔ 𝜃 ) )
5		frpoins3xp3g.5	⊢ ( 𝑥 = 𝑋 → ( 𝜑 ↔ 𝜏 ) )
6		frpoins3xp3g.6	⊢ ( 𝑦 = 𝑌 → ( 𝜏 ↔ 𝜂 ) )
7		frpoins3xp3g.7	⊢ ( 𝑧 = 𝑍 → ( 𝜂 ↔ 𝜁 ) )
8	2	sbcbidv	⊢ ( 𝑥 = 𝑤 → ( [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ↔ [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜓 ) )
9	8	sbcbidv	⊢ ( 𝑥 = 𝑤 → ( [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ↔ [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜓 ) )
10	9	cbvsbcvw	⊢ ( [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ↔ [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜓 )
11	3	sbcbidv	⊢ ( 𝑦 = 𝑡 → ( [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜓 ↔ [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜒 ) )
12	11	cbvsbcvw	⊢ ( [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜓 ↔ [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜒 )
13	4	cbvsbcvw	⊢ ( [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜒 ↔ [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
14	13	sbcbii	⊢ ( [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜒 ↔ [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
15	12 14	bitri	⊢ ( [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜓 ↔ [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
16	15	sbcbii	⊢ ( [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜓 ↔ [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
17	10 16	bitri	⊢ ( [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ↔ [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
18	17	ralbii	⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ↔ ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
19		elxpxp	⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
20		nfv	⊢ Ⅎ 𝑥 ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
21		nfsbc1v	⊢ Ⅎ 𝑥 [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑
22	20 21	nfim	⊢ Ⅎ 𝑥 ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 )
23		nfv	⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
24		nfv	⊢ Ⅎ 𝑦 ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
25		nfcv	⊢ Ⅎ 𝑦 ( 1^st ‘ ( 1^st ‘ 𝑝 ) )
26		nfsbc1v	⊢ Ⅎ 𝑦 [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑
27	25 26	nfsbcw	⊢ Ⅎ 𝑦 [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑
28	24 27	nfim	⊢ Ⅎ 𝑦 ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 )
29		nfv	⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 )
30		nfv	⊢ Ⅎ 𝑧 ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
31		nfcv	⊢ Ⅎ 𝑧 ( 1^st ‘ ( 1^st ‘ 𝑝 ) )
32		nfcv	⊢ Ⅎ 𝑧 ( 2^nd ‘ ( 1^st ‘ 𝑝 ) )
33		nfsbc1v	⊢ Ⅎ 𝑧 [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑
34	32 33	nfsbcw	⊢ Ⅎ 𝑧 [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑
35	31 34	nfsbcw	⊢ Ⅎ 𝑧 [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑
36	30 35	nfim	⊢ Ⅎ 𝑧 ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 )
37		impexp	⊢ ( ( ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) )
38		elin	⊢ ( 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) )
39		predss	⊢ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 )
40		sseqin2	⊢ ( Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) = Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
41	39 40	mpbi	⊢ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) = Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
42	41	eleq2i	⊢ ( 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) ↔ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
43	38 42	bitr3i	⊢ ( ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) ↔ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
44	43	imbi1i	⊢ ( ( ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) )
45	37 44	bitr3i	⊢ ( ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) ↔ ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) )
46	45	albii	⊢ ( ∀ 𝑞 ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) ↔ ∀ 𝑞 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) )
47		r3al	⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ↔ ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
48		nfv	⊢ Ⅎ 𝑤 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
49		nfsbc1v	⊢ Ⅎ 𝑤 [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
50	48 49	nfim	⊢ Ⅎ 𝑤 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
51		nfv	⊢ Ⅎ 𝑡 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
52		nfcv	⊢ Ⅎ 𝑡 ( 1^st ‘ ( 1^st ‘ 𝑞 ) )
53		nfsbc1v	⊢ Ⅎ 𝑡 [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
54	52 53	nfsbcw	⊢ Ⅎ 𝑡 [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
55	51 54	nfim	⊢ Ⅎ 𝑡 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
56		nfv	⊢ Ⅎ 𝑢 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
57		nfcv	⊢ Ⅎ 𝑢 ( 1^st ‘ ( 1^st ‘ 𝑞 ) )
58		nfcv	⊢ Ⅎ 𝑢 ( 2^nd ‘ ( 1^st ‘ 𝑞 ) )
59		nfsbc1v	⊢ Ⅎ 𝑢 [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
60	58 59	nfsbcw	⊢ Ⅎ 𝑢 [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
61	57 60	nfsbcw	⊢ Ⅎ 𝑢 [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
62	56 61	nfim	⊢ Ⅎ 𝑢 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
63		nfv	⊢ Ⅎ 𝑞 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 )
64		eleq1	⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ↔ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) )
65		sbcoteq1a	⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ↔ 𝜃 ) )
66	64 65	imbi12d	⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
67	50 55 62 63 66	ralxp3f	⊢ ( ∀ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) )
68		elin	⊢ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) ↔ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) )
69	41	eleq2i	⊢ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) ↔ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
70	68 69	bitr3i	⊢ ( ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) ↔ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
71	70	imbi1i	⊢ ( ( ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) → 𝜃 ) ↔ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) )
72		impexp	⊢ ( ( ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) ) → 𝜃 ) ↔ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
73	71 72	bitr3i	⊢ ( ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ↔ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
74		ot2elxp	⊢ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) )
75	74	imbi1i	⊢ ( ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
76	73 75	bitri	⊢ ( ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
77	76	albii	⊢ ( ∀ 𝑢 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ↔ ∀ 𝑢 ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
78	77	2albii	⊢ ( ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ↔ ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ) )
79	47 67 78	3bitr4ri	⊢ ( ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ↔ ∀ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) )
80		df-ral	⊢ ( ∀ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ∀ 𝑞 ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) )
81	79 80	bitri	⊢ ( ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) ↔ ∀ 𝑞 ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) )
82		df-ral	⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ↔ ∀ 𝑞 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) )
83	46 81 82	3bitr4ri	⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ↔ ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → 𝜃 ) )
84	83 1	syl5bi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → 𝜑 ) )
85		predeq3	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) = Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
86	85	raleqdv	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ↔ ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) )
87		sbcoteq1a	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ↔ 𝜑 ) )
88	86 87	imbi12d	⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ( ∀ 𝑞 ∈ 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 ‘ 𝑞 ) / 𝑢 ] 𝜃 → 𝜑 ) ) )
89	84 88	syl5ibrcom	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) ) )
90	89	3expia	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∈ 𝐶 → ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) ) ) )
91	29 36 90	rexlimd	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑧 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) ) )
92	91	ex	⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( ∃ 𝑧 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) ) ) )
93	23 28 92	rexlimd	⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) ) )
94	22 93	rexlimi	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) )
95	19 94	sylbi	⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) )
96	18 95	syl5bi	⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , 𝑝 ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 → [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ) )
97		2fveq3	⊢ ( 𝑝 = 𝑞 → ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) )
98		2fveq3	⊢ ( 𝑝 = 𝑞 → ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) )
99		fveq2	⊢ ( 𝑝 = 𝑞 → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ 𝑞 ) )
100	99	sbceq1d	⊢ ( 𝑝 = 𝑞 → ( [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ↔ [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ) )
101	98 100	sbceqbid	⊢ ( 𝑝 = 𝑞 → ( [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ↔ [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ) )
102	97 101	sbceqbid	⊢ ( 𝑝 = 𝑞 → ( [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ↔ [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑞 ) / 𝑧 ] 𝜑 ) )
103	96 102	frpoins2g	⊢ ( ( 𝑅 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑅 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑅 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ∀ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 )
104		ralxp3es	⊢ ( ∀ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) [ ( 1^st ‘ ( 1^st ‘ 𝑝 ) ) / 𝑥 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑝 ) ) / 𝑦 ] [ ( 2^nd ‘ 𝑝 ) / 𝑧 ] 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 )
105	103 104	sylib	⊢ ( ( 𝑅 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑅 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑅 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 )
106	5 6 7	rspc3v	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐶 𝜑 → 𝜁 ) )
107	105 106	mpan9	⊢ ( ( ( 𝑅 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑅 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑅 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝜁 )

Metamath Proof Explorer

Theorem frpoins3xp3g

Proof