MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  frpoins3xp3g Structured version   Visualization version   GIF version

Theorem frpoins3xp3g 8078
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.
StepHypRef Expression
1 frpoins3xp3g.2 . . . . . . . . . 10 (𝑥 = 𝑤 → (𝜑𝜓))
21sbcbidv 3803 . . . . . . . . 9 (𝑥 = 𝑤 → ([(2nd𝑞) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜓))
32sbcbidv 3803 . . . . . . . 8 (𝑥 = 𝑤 → ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓))
43cbvsbcvw 3779 . . . . . . 7 ([(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓)
5 frpoins3xp3g.3 . . . . . . . . . . 11 (𝑦 = 𝑡 → (𝜓𝜒))
65sbcbidv 3803 . . . . . . . . . 10 (𝑦 = 𝑡 → ([(2nd𝑞) / 𝑧]𝜓[(2nd𝑞) / 𝑧]𝜒))
76cbvsbcvw 3779 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒)
8 frpoins3xp3g.4 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝜒𝜃))
98cbvsbcvw 3779 . . . . . . . . . 10 ([(2nd𝑞) / 𝑧]𝜒[(2nd𝑞) / 𝑢]𝜃)
109sbcbii 3804 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
117, 10bitri 275 . . . . . . . 8 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
1211sbcbii 3804 . . . . . . 7 ([(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
134, 12bitri 275 . . . . . 6 ([(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
1413ralbii 3097 . . . . 5 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
15 el2xptp 7972 . . . . . 6 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥𝐴𝑦𝐵𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩)
16 nfv 1918 . . . . . . . 8 𝑥𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
17 nfsbc1v 3764 . . . . . . . 8 𝑥[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
1816, 17nfim 1900 . . . . . . 7 𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
19 nfv 1918 . . . . . . . 8 𝑦 𝑥𝐴
20 nfv 1918 . . . . . . . . 9 𝑦𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
21 nfcv 2908 . . . . . . . . . 10 𝑦(1st ‘(1st𝑝))
22 nfsbc1v 3764 . . . . . . . . . 10 𝑦[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2321, 22nfsbcw 3766 . . . . . . . . 9 𝑦[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2420, 23nfim 1900 . . . . . . . 8 𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
25 nfv 1918 . . . . . . . . . 10 𝑧(𝑥𝐴𝑦𝐵)
26 nfv 1918 . . . . . . . . . . 11 𝑧𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
27 nfcv 2908 . . . . . . . . . . . 12 𝑧(1st ‘(1st𝑝))
28 nfcv 2908 . . . . . . . . . . . . 13 𝑧(2nd ‘(1st𝑝))
29 nfsbc1v 3764 . . . . . . . . . . . . 13 𝑧[(2nd𝑝) / 𝑧]𝜑
3028, 29nfsbcw 3766 . . . . . . . . . . . 12 𝑧[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3127, 30nfsbcw 3766 . . . . . . . . . . 11 𝑧[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3226, 31nfim 1900 . . . . . . . . . 10 𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
33 predss 6266 . . . . . . . . . . . . . . . . . . . . . 22 Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
34 sseqin2 4180 . . . . . . . . . . . . . . . . . . . . . 22 (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
3533, 34mpbi 229 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
3635eleq2i 2830 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
3736bicomi 223 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
38 elin 3931 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
3937, 38bitri 275 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
4039imbi1i 350 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
41 impexp 452 . . . . . . . . . . . . . . . . 17 (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
4240, 41bitri 275 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
4342albii 1822 . . . . . . . . . . . . . . 15 (∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
4443bicomi 223 . . . . . . . . . . . . . 14 (∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
45 r3al 3194 . . . . . . . . . . . . . . . 16 (∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
46 nfv 1918 . . . . . . . . . . . . . . . . . 18 𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
47 nfsbc1v 3764 . . . . . . . . . . . . . . . . . 18 𝑤[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
4846, 47nfim 1900 . . . . . . . . . . . . . . . . 17 𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
49 nfv 1918 . . . . . . . . . . . . . . . . . 18 𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
50 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑡(1st ‘(1st𝑞))
51 nfsbc1v 3764 . . . . . . . . . . . . . . . . . . 19 𝑡[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5250, 51nfsbcw 3766 . . . . . . . . . . . . . . . . . 18 𝑡[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5349, 52nfim 1900 . . . . . . . . . . . . . . . . 17 𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
54 nfv 1918 . . . . . . . . . . . . . . . . . 18 𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
55 nfcv 2908 . . . . . . . . . . . . . . . . . . 19 𝑢(1st ‘(1st𝑞))
56 nfcv 2908 . . . . . . . . . . . . . . . . . . . 20 𝑢(2nd ‘(1st𝑞))
57 nfsbc1v 3764 . . . . . . . . . . . . . . . . . . . 20 𝑢[(2nd𝑞) / 𝑢]𝜃
5856, 57nfsbcw 3766 . . . . . . . . . . . . . . . . . . 19 𝑢[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5955, 58nfsbcw 3766 . . . . . . . . . . . . . . . . . 18 𝑢[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
6054, 59nfim 1900 . . . . . . . . . . . . . . . . 17 𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
61 nfv 1918 . . . . . . . . . . . . . . . . 17 𝑞(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)
62 eleq1 2826 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
63 sbcoteq1a 7988 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ([(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜃))
6462, 63imbi12d 345 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
6548, 53, 60, 61, 64ralxp3f 8074 . . . . . . . . . . . . . . . 16 (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
66 elin 3931 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
6735eleq2i 2830 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
68 otelxp 5681 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤𝐴𝑡𝐵𝑢𝐶))
6968anbi1i 625 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
7066, 67, 693bitr3i 301 . . . . . . . . . . . . . . . . . . 19 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
7170imbi1i 350 . . . . . . . . . . . . . . . . . 18 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ (((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃))
72 impexp 452 . . . . . . . . . . . . . . . . . 18 ((((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
7371, 72bitri 275 . . . . . . . . . . . . . . . . 17 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
74733albii 1824 . . . . . . . . . . . . . . . 16 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
7545, 65, 743bitr4ri 304 . . . . . . . . . . . . . . 15 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
76 df-ral 3066 . . . . . . . . . . . . . . 15 (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
7775, 76bitri 275 . . . . . . . . . . . . . 14 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
78 df-ral 3066 . . . . . . . . . . . . . 14 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
7944, 77, 783bitr4ri 304 . . . . . . . . . . . . 13 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
80 frpoins3xp3g.1 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐵𝑧𝐶) → (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) → 𝜑))
8179, 80biimtrid 241 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐵𝑧𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜑))
82 predeq3 6262 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
8382raleqdv 3316 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
84 sbcoteq1a 7988 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑𝜑))
8583, 84imbi12d 345 . . . . . . . . . . . 12 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → ((∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑) ↔ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜑)))
8681, 85syl5ibrcom 247 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐵𝑧𝐶) → (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
87863expia 1122 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐵) → (𝑧𝐶 → (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
8825, 32, 87rexlimd 3252 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → (∃𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
8988ex 414 . . . . . . . 8 (𝑥𝐴 → (𝑦𝐵 → (∃𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
9019, 24, 89rexlimd 3252 . . . . . . 7 (𝑥𝐴 → (∃𝑦𝐵𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
9118, 90rexlimi 3245 . . . . . 6 (∃𝑥𝐴𝑦𝐵𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))
9215, 91sylbi 216 . . . . 5 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))
9314, 92biimtrid 241 . . . 4 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))
94 2fveq3 6852 . . . . 5 (𝑝 = 𝑞 → (1st ‘(1st𝑝)) = (1st ‘(1st𝑞)))
95 2fveq3 6852 . . . . . 6 (𝑝 = 𝑞 → (2nd ‘(1st𝑝)) = (2nd ‘(1st𝑞)))
96 fveq2 6847 . . . . . . 7 (𝑝 = 𝑞 → (2nd𝑝) = (2nd𝑞))
9796sbceq1d 3749 . . . . . 6 (𝑝 = 𝑞 → ([(2nd𝑝) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜑))
9895, 97sbceqbid 3751 . . . . 5 (𝑝 = 𝑞 → ([(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
9994, 98sbceqbid 3751 . . . 4 (𝑝 = 𝑞 → ([(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
10093, 99frpoins2g 6304 . . 3 ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
101 ralxp3es 8076 . . 3 (∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑 ↔ ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑)
102100, 101sylib 217 . 2 ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑)
103 frpoins3xp3g.5 . . 3 (𝑥 = 𝑋 → (𝜑𝜏))
104 frpoins3xp3g.6 . . 3 (𝑦 = 𝑌 → (𝜏𝜂))
105 frpoins3xp3g.7 . . 3 (𝑧 = 𝑍 → (𝜂𝜁))
106103, 104, 105rspc3v 3596 . 2 ((𝑋𝐴𝑌𝐵𝑍𝐶) → (∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑𝜁))
107102, 106mpan9 508 1 (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋𝐴𝑌𝐵𝑍𝐶)) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088  wal 1540   = wceq 1542  wcel 2107  wral 3065  wrex 3074  [wsbc 3744  cin 3914  wss 3915  cotp 4599   Po wpo 5548   Fr wfr 5590   Se wse 5591   × cxp 5636  Predcpred 6257  cfv 6501  1st c1st 7924  2nd c2nd 7925
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-ot 4600  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-po 5550  df-fr 5593  df-se 5594  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-iota 6453  df-fun 6503  df-fv 6509  df-1st 7926  df-2nd 7927
This theorem is referenced by:  xpord3inddlem  8091
  Copyright terms: Public domain W3C validator