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

Theorem frpoins3xp3g 8132
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 3836 . . . . . . . . 9 (𝑥 = 𝑤 → ([(2nd𝑞) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜓))
32sbcbidv 3836 . . . . . . . 8 (𝑥 = 𝑤 → ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓))
43cbvsbcvw 3812 . . . . . . 7 ([(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓)
5 frpoins3xp3g.3 . . . . . . . . . . 11 (𝑦 = 𝑡 → (𝜓𝜒))
65sbcbidv 3836 . . . . . . . . . 10 (𝑦 = 𝑡 → ([(2nd𝑞) / 𝑧]𝜓[(2nd𝑞) / 𝑧]𝜒))
76cbvsbcvw 3812 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒)
8 frpoins3xp3g.4 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝜒𝜃))
98cbvsbcvw 3812 . . . . . . . . . 10 ([(2nd𝑞) / 𝑧]𝜒[(2nd𝑞) / 𝑢]𝜃)
109sbcbii 3837 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
117, 10bitri 275 . . . . . . . 8 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
1211sbcbii 3837 . . . . . . 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 3092 . . . . 5 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
15 el2xptp 8025 . . . . . 6 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥𝐴𝑦𝐵𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩)
16 nfv 1916 . . . . . . . 8 𝑥𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
17 nfsbc1v 3797 . . . . . . . 8 𝑥[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
1816, 17nfim 1898 . . . . . . 7 𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
19 nfv 1916 . . . . . . . 8 𝑦 𝑥𝐴
20 nfv 1916 . . . . . . . . 9 𝑦𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
21 nfcv 2902 . . . . . . . . . 10 𝑦(1st ‘(1st𝑝))
22 nfsbc1v 3797 . . . . . . . . . 10 𝑦[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2321, 22nfsbcw 3799 . . . . . . . . 9 𝑦[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2420, 23nfim 1898 . . . . . . . 8 𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
25 nfv 1916 . . . . . . . . . 10 𝑧(𝑥𝐴𝑦𝐵)
26 nfv 1916 . . . . . . . . . . 11 𝑧𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
27 nfcv 2902 . . . . . . . . . . . 12 𝑧(1st ‘(1st𝑝))
28 nfcv 2902 . . . . . . . . . . . . 13 𝑧(2nd ‘(1st𝑝))
29 nfsbc1v 3797 . . . . . . . . . . . . 13 𝑧[(2nd𝑝) / 𝑧]𝜑
3028, 29nfsbcw 3799 . . . . . . . . . . . 12 𝑧[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3127, 30nfsbcw 3799 . . . . . . . . . . 11 𝑧[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3226, 31nfim 1898 . . . . . . . . . 10 𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
33 predss 6308 . . . . . . . . . . . . . . . . . . . . . 22 Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
34 sseqin2 4215 . . . . . . . . . . . . . . . . . . . . . 22 (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
3533, 34mpbi 229 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
3635eleq2i 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
3736bicomi 223 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
38 elin 3964 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
3937, 38bitri 275 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
4039imbi1i 349 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
41 impexp 450 . . . . . . . . . . . . . . . . 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 1820 . . . . . . . . . . . . . . 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 3195 . . . . . . . . . . . . . . . 16 (∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
46 nfv 1916 . . . . . . . . . . . . . . . . . 18 𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
47 nfsbc1v 3797 . . . . . . . . . . . . . . . . . 18 𝑤[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
4846, 47nfim 1898 . . . . . . . . . . . . . . . . 17 𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
49 nfv 1916 . . . . . . . . . . . . . . . . . 18 𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
50 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑡(1st ‘(1st𝑞))
51 nfsbc1v 3797 . . . . . . . . . . . . . . . . . . 19 𝑡[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5250, 51nfsbcw 3799 . . . . . . . . . . . . . . . . . 18 𝑡[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5349, 52nfim 1898 . . . . . . . . . . . . . . . . 17 𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
54 nfv 1916 . . . . . . . . . . . . . . . . . 18 𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
55 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑢(1st ‘(1st𝑞))
56 nfcv 2902 . . . . . . . . . . . . . . . . . . . 20 𝑢(2nd ‘(1st𝑞))
57 nfsbc1v 3797 . . . . . . . . . . . . . . . . . . . 20 𝑢[(2nd𝑞) / 𝑢]𝜃
5856, 57nfsbcw 3799 . . . . . . . . . . . . . . . . . . 19 𝑢[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5955, 58nfsbcw 3799 . . . . . . . . . . . . . . . . . 18 𝑢[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
6054, 59nfim 1898 . . . . . . . . . . . . . . . . 17 𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
61 nfv 1916 . . . . . . . . . . . . . . . . 17 𝑞(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)
62 eleq1 2820 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
63 sbcoteq1a 8041 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ([(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜃))
6462, 63imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
6548, 53, 60, 61, 64ralxp3f 8128 . . . . . . . . . . . . . . . 16 (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
66 elin 3964 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
6735eleq2i 2824 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
68 otelxp 5720 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤𝐴𝑡𝐵𝑢𝐶))
6968anbi1i 623 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
7066, 67, 693bitr3i 301 . . . . . . . . . . . . . . . . . . 19 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
7170imbi1i 349 . . . . . . . . . . . . . . . . . 18 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ (((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃))
72 impexp 450 . . . . . . . . . . . . . . . . . 18 ((((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
7371, 72bitri 275 . . . . . . . . . . . . . . . . 17 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
74733albii 1822 . . . . . . . . . . . . . . . 16 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
7545, 65, 743bitr4ri 304 . . . . . . . . . . . . . . 15 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
76 df-ral 3061 . . . . . . . . . . . . . . 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 3061 . . . . . . . . . . . . . 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 6304 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
8382raleqdv 3324 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
84 sbcoteq1a 8041 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → ([(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑𝜑))
8583, 84imbi12d 344 . . . . . . . . . . . 12 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → ((∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑) ↔ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜑)))
8681, 85syl5ibrcom 246 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐵𝑧𝐶) → (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
87863expia 1120 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐵) → (𝑧𝐶 → (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
8825, 32, 87rexlimd 3262 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → (∃𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
8988ex 412 . . . . . . . 8 (𝑥𝐴 → (𝑦𝐵 → (∃𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
9019, 24, 89rexlimd 3262 . . . . . . 7 (𝑥𝐴 → (∃𝑦𝐵𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
9118, 90rexlimi 3255 . . . . . 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 6896 . . . . 5 (𝑝 = 𝑞 → (1st ‘(1st𝑝)) = (1st ‘(1st𝑞)))
95 2fveq3 6896 . . . . . 6 (𝑝 = 𝑞 → (2nd ‘(1st𝑝)) = (2nd ‘(1st𝑞)))
96 fveq2 6891 . . . . . . 7 (𝑝 = 𝑞 → (2nd𝑝) = (2nd𝑞))
9796sbceq1d 3782 . . . . . 6 (𝑝 = 𝑞 → ([(2nd𝑝) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜑))
9895, 97sbceqbid 3784 . . . . 5 (𝑝 = 𝑞 → ([(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
9994, 98sbceqbid 3784 . . . 4 (𝑝 = 𝑞 → ([(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
10093, 99frpoins2g 6346 . . 3 ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
101 ralxp3es 8130 . . 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 3627 . 2 ((𝑋𝐴𝑌𝐵𝑍𝐶) → (∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑𝜁))
107102, 106mpan9 506 1 (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋𝐴𝑌𝐵𝑍𝐶)) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3a 1086  wal 1538   = wceq 1540  wcel 2105  wral 3060  wrex 3069  [wsbc 3777  cin 3947  wss 3948  cotp 4636   Po wpo 5586   Fr wfr 5628   Se wse 5629   × cxp 5674  Predcpred 6299  cfv 6543  1st c1st 7977  2nd c2nd 7978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-ot 4637  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-fr 5631  df-se 5632  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fun 6545  df-fv 6551  df-1st 7979  df-2nd 7980
This theorem is referenced by:  xpord3inddlem  8145
  Copyright terms: Public domain W3C validator