frpoins3xp3g

Description: Special case of founded partial recursion over a triple Cartesian 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		el2xptp	⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∃ 𝑧 ∈ 𝐶 𝑝 = ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
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		predss	⊢ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 )
38		sseqin2	⊢ ( Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) = Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
39	37 38	mpbi	⊢ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) = Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
40	39	eleq2i	⊢ ( 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
41	40	bicomi	⊢ ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ↔ 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
42		elin	⊢ ( 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
43	41 42	bitri	⊢ ( 𝑞 ∈ 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		impexp	⊢ ( ( ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) )
46	44 45	bitri	⊢ ( ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) )
47	46	albii	⊢ ( ∀ 𝑞 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ∀ 𝑞 ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) )
48	47	bicomi	⊢ ( ∀ 𝑞 ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ) ↔ ∀ 𝑞 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) )
49		r3al	⊢ ( ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ↔ ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ) )
50		nfv	⊢ Ⅎ 𝑤 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
51		nfsbc1v	⊢ Ⅎ 𝑤 [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
52	50 51	nfim	⊢ Ⅎ 𝑤 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
53		nfv	⊢ Ⅎ 𝑡 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
54		nfcv	⊢ Ⅎ 𝑡 ( 1^st ‘ ( 1^st ‘ 𝑞 ) )
55		nfsbc1v	⊢ Ⅎ 𝑡 [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
56	54 55	nfsbcw	⊢ Ⅎ 𝑡 [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
57	53 56	nfim	⊢ Ⅎ 𝑡 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
58		nfv	⊢ Ⅎ 𝑢 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ )
59		nfcv	⊢ Ⅎ 𝑢 ( 1^st ‘ ( 1^st ‘ 𝑞 ) )
60		nfcv	⊢ Ⅎ 𝑢 ( 2^nd ‘ ( 1^st ‘ 𝑞 ) )
61		nfsbc1v	⊢ Ⅎ 𝑢 [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
62	60 61	nfsbcw	⊢ Ⅎ 𝑢 [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
63	59 62	nfsbcw	⊢ Ⅎ 𝑢 [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃
64	58 63	nfim	⊢ Ⅎ 𝑢 ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 )
65		nfv	⊢ Ⅎ 𝑞 ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 )
66		eleq1	⊢ ( 𝑞 = ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ → ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ↔ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
67		sbcoteq1a	⊢ ( 𝑞 = ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ → ( [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ↔ 𝜃 ) )
68	66 67	imbi12d	⊢ ( 𝑞 = ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ → ( ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ) )
69	52 57 64 65 68	ralxp3f	⊢ ( ∀ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ( 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ) ↔ ∀ 𝑤 ∈ 𝐴 ∀ 𝑡 ∈ 𝐵 ∀ 𝑢 ∈ 𝐶 ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) )
70		elin	⊢ ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
71	39	eleq2i	⊢ ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) )
72		otelxp	⊢ ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) )
73	72	anbi1i	⊢ ( ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) ∧ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
74	70 71 73	3bitr3i	⊢ ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) ∧ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) )
75	74	imbi1i	⊢ ( ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ↔ ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) ∧ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) → 𝜃 ) )
76		impexp	⊢ ( ( ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) ∧ ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) ) → 𝜃 ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ) )
77	75 76	bitri	⊢ ( ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ↔ ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ) )
78	77	3albii	⊢ ( ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ↔ ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ( 𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐶 ) → ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) ) )
79	49 69 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	48 81 82	3bitr4ri	⊢ ( ∀ 𝑞 ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) [ ( 1^st ‘ ( 1^st ‘ 𝑞 ) ) / 𝑤 ] [ ( 2^nd ‘ ( 1^st ‘ 𝑞 ) ) / 𝑡 ] [ ( 2^nd ‘ 𝑞 ) / 𝑢 ] 𝜃 ↔ ∀ 𝑤 ∀ 𝑡 ∀ 𝑢 ( ⟨ 𝑤 , 𝑡 , 𝑢 ⟩ ∈ Pred ( 𝑅 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑥 , 𝑦 , 𝑧 ⟩ ) → 𝜃 ) )
84	83 1	biimtrid	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) → ( ∀ 𝑞 ∈ 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	biimtrid	⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( ∀ 𝑞 ∈ 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