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

Theorem frpoins3xp3g 8073
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 3798 . . . . . . . . 9 (𝑥 = 𝑤 → ([(2nd𝑞) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜓))
32sbcbidv 3798 . . . . . . . 8 (𝑥 = 𝑤 → ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓))
43cbvsbcvw 3774 . . . . . . 7 ([(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓)
5 frpoins3xp3g.3 . . . . . . . . . . 11 (𝑦 = 𝑡 → (𝜓𝜒))
65sbcbidv 3798 . . . . . . . . . 10 (𝑦 = 𝑡 → ([(2nd𝑞) / 𝑧]𝜓[(2nd𝑞) / 𝑧]𝜒))
76cbvsbcvw 3774 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒)
8 frpoins3xp3g.4 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝜒𝜃))
98cbvsbcvw 3774 . . . . . . . . . 10 ([(2nd𝑞) / 𝑧]𝜒[(2nd𝑞) / 𝑢]𝜃)
109sbcbii 3799 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
117, 10bitri 274 . . . . . . . 8 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
1211sbcbii 3799 . . . . . . 7 ([(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
134, 12bitri 274 . . . . . 6 ([(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
1413ralbii 3096 . . . . 5 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
15 el2xptp 7967 . . . . . 6 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥𝐴𝑦𝐵𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩)
16 nfv 1917 . . . . . . . 8 𝑥𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
17 nfsbc1v 3759 . . . . . . . 8 𝑥[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
1816, 17nfim 1899 . . . . . . 7 𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
19 nfv 1917 . . . . . . . 8 𝑦 𝑥𝐴
20 nfv 1917 . . . . . . . . 9 𝑦𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
21 nfcv 2907 . . . . . . . . . 10 𝑦(1st ‘(1st𝑝))
22 nfsbc1v 3759 . . . . . . . . . 10 𝑦[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2321, 22nfsbcw 3761 . . . . . . . . 9 𝑦[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2420, 23nfim 1899 . . . . . . . 8 𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
25 nfv 1917 . . . . . . . . . 10 𝑧(𝑥𝐴𝑦𝐵)
26 nfv 1917 . . . . . . . . . . 11 𝑧𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
27 nfcv 2907 . . . . . . . . . . . 12 𝑧(1st ‘(1st𝑝))
28 nfcv 2907 . . . . . . . . . . . . 13 𝑧(2nd ‘(1st𝑝))
29 nfsbc1v 3759 . . . . . . . . . . . . 13 𝑧[(2nd𝑝) / 𝑧]𝜑
3028, 29nfsbcw 3761 . . . . . . . . . . . 12 𝑧[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3127, 30nfsbcw 3761 . . . . . . . . . . 11 𝑧[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3226, 31nfim 1899 . . . . . . . . . 10 𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
33 predss 6261 . . . . . . . . . . . . . . . . . . . . . 22 Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
34 sseqin2 4175 . . . . . . . . . . . . . . . . . . . . . 22 (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
3533, 34mpbi 229 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
3635eleq2i 2829 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
3736bicomi 223 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
38 elin 3926 . . . . . . . . . . . . . . . . . . 19 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
3937, 38bitri 274 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
4039imbi1i 349 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
41 impexp 451 . . . . . . . . . . . . . . . . 17 (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
4240, 41bitri 274 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
4342albii 1821 . . . . . . . . . . . . . . 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 3193 . . . . . . . . . . . . . . . 16 (∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
46 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
47 nfsbc1v 3759 . . . . . . . . . . . . . . . . . 18 𝑤[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
4846, 47nfim 1899 . . . . . . . . . . . . . . . . 17 𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
49 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
50 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑡(1st ‘(1st𝑞))
51 nfsbc1v 3759 . . . . . . . . . . . . . . . . . . 19 𝑡[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5250, 51nfsbcw 3761 . . . . . . . . . . . . . . . . . 18 𝑡[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5349, 52nfim 1899 . . . . . . . . . . . . . . . . 17 𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
54 nfv 1917 . . . . . . . . . . . . . . . . . 18 𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)
55 nfcv 2907 . . . . . . . . . . . . . . . . . . 19 𝑢(1st ‘(1st𝑞))
56 nfcv 2907 . . . . . . . . . . . . . . . . . . . 20 𝑢(2nd ‘(1st𝑞))
57 nfsbc1v 3759 . . . . . . . . . . . . . . . . . . . 20 𝑢[(2nd𝑞) / 𝑢]𝜃
5856, 57nfsbcw 3761 . . . . . . . . . . . . . . . . . . 19 𝑢[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5955, 58nfsbcw 3761 . . . . . . . . . . . . . . . . . 18 𝑢[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
6054, 59nfim 1899 . . . . . . . . . . . . . . . . 17 𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
61 nfv 1917 . . . . . . . . . . . . . . . . 17 𝑞(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)
62 eleq1 2825 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
63 sbcoteq1a 7983 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ([(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜃))
6462, 63imbi12d 344 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨𝑤, 𝑡, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
6548, 53, 60, 61, 64ralxp3f 8069 . . . . . . . . . . . . . . . 16 (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃))
66 elin 3926 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
6735eleq2i 2829 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑤, 𝑡, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
68 otelxp 5676 . . . . . . . . . . . . . . . . . . . . 21 (⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤𝐴𝑡𝐵𝑢𝐶))
6968anbi1i 624 . . . . . . . . . . . . . . . . . . . 20 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
7066, 67, 693bitr3i 300 . . . . . . . . . . . . . . . . . . 19 (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)))
7170imbi1i 349 . . . . . . . . . . . . . . . . . 18 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ (((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃))
72 impexp 451 . . . . . . . . . . . . . . . . . 18 ((((𝑤𝐴𝑡𝐵𝑢𝐶) ∧ ⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)) → 𝜃) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
7371, 72bitri 274 . . . . . . . . . . . . . . . . 17 ((⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
74733albii 1823 . . . . . . . . . . . . . . . 16 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃)))
7545, 65, 743bitr4ri 303 . . . . . . . . . . . . . . 15 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
76 df-ral 3065 . . . . . . . . . . . . . . 15 (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
7775, 76bitri 274 . . . . . . . . . . . . . 14 (∀𝑤𝑡𝑢(⟨𝑤, 𝑡, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
78 df-ral 3065 . . . . . . . . . . . . . 14 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
7944, 77, 783bitr4ri 303 . . . . . . . . . . . . 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 6257 . . . . . . . . . . . . . 14 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩))
8382raleqdv 3313 . . . . . . . . . . . . 13 (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨𝑥, 𝑦, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
84 sbcoteq1a 7983 . . . . . . . . . . . . 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 1121 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐵) → (𝑧𝐶 → (𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
8825, 32, 87rexlimd 3249 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → (∃𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
8988ex 413 . . . . . . . 8 (𝑥𝐴 → (𝑦𝐵 → (∃𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
9019, 24, 89rexlimd 3249 . . . . . . 7 (𝑥𝐴 → (∃𝑦𝐵𝑧𝐶 𝑝 = ⟨𝑥, 𝑦, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
9118, 90rexlimi 3242 . . . . . 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 6847 . . . . 5 (𝑝 = 𝑞 → (1st ‘(1st𝑝)) = (1st ‘(1st𝑞)))
95 2fveq3 6847 . . . . . 6 (𝑝 = 𝑞 → (2nd ‘(1st𝑝)) = (2nd ‘(1st𝑞)))
96 fveq2 6842 . . . . . . 7 (𝑝 = 𝑞 → (2nd𝑝) = (2nd𝑞))
9796sbceq1d 3744 . . . . . 6 (𝑝 = 𝑞 → ([(2nd𝑝) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜑))
9895, 97sbceqbid 3746 . . . . 5 (𝑝 = 𝑞 → ([(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
9994, 98sbceqbid 3746 . . . 4 (𝑝 = 𝑞 → ([(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
10093, 99frpoins2g 6299 . . 3 ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
101 ralxp3es 8071 . . 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 3593 . 2 ((𝑋𝐴𝑌𝐵𝑍𝐶) → (∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑𝜁))
107102, 106mpan9 507 1 (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋𝐴𝑌𝐵𝑍𝐶)) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087  wal 1539   = wceq 1541  wcel 2106  wral 3064  wrex 3073  [wsbc 3739  cin 3909  wss 3910  cotp 4594   Po wpo 5543   Fr wfr 5585   Se wse 5586   × cxp 5631  Predcpred 6252  cfv 6496  1st c1st 7919  2nd c2nd 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-ot 4595  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-fr 5588  df-se 5589  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922
This theorem is referenced by:  xpord3inddlem  8086
  Copyright terms: Public domain W3C validator