Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frpoins3xp3g Structured version   Visualization version   GIF version

Theorem frpoins3xp3g 33554
Description: Special case of founded partial recursion over a triple cross 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 3768 . . . . . . . . 9 (𝑥 = 𝑤 → ([(2nd𝑞) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜓))
32sbcbidv 3768 . . . . . . . 8 (𝑥 = 𝑤 → ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓))
43cbvsbcvw 3744 . . . . . . 7 ([(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓)
5 frpoins3xp3g.3 . . . . . . . . . . 11 (𝑦 = 𝑡 → (𝜓𝜒))
65sbcbidv 3768 . . . . . . . . . 10 (𝑦 = 𝑡 → ([(2nd𝑞) / 𝑧]𝜓[(2nd𝑞) / 𝑧]𝜒))
76cbvsbcvw 3744 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒)
8 frpoins3xp3g.4 . . . . . . . . . . 11 (𝑧 = 𝑢 → (𝜒𝜃))
98cbvsbcvw 3744 . . . . . . . . . 10 ([(2nd𝑞) / 𝑧]𝜒[(2nd𝑞) / 𝑢]𝜃)
109sbcbii 3770 . . . . . . . . 9 ([(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑧]𝜒[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
117, 10bitri 278 . . . . . . . 8 ([(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
1211sbcbii 3770 . . . . . . 7 ([(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜓[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
134, 12bitri 278 . . . . . 6 ([(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
1413ralbii 3089 . . . . 5 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
15 elxpxp 33425 . . . . . 6 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑥𝐴𝑦𝐵𝑧𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
16 nfv 1922 . . . . . . . 8 𝑥𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
17 nfsbc1v 3729 . . . . . . . 8 𝑥[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
1816, 17nfim 1904 . . . . . . 7 𝑥(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
19 nfv 1922 . . . . . . . 8 𝑦 𝑥𝐴
20 nfv 1922 . . . . . . . . 9 𝑦𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
21 nfcv 2905 . . . . . . . . . 10 𝑦(1st ‘(1st𝑝))
22 nfsbc1v 3729 . . . . . . . . . 10 𝑦[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2321, 22nfsbcw 3731 . . . . . . . . 9 𝑦[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
2420, 23nfim 1904 . . . . . . . 8 𝑦(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
25 nfv 1922 . . . . . . . . . 10 𝑧(𝑥𝐴𝑦𝐵)
26 nfv 1922 . . . . . . . . . . 11 𝑧𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
27 nfcv 2905 . . . . . . . . . . . 12 𝑧(1st ‘(1st𝑝))
28 nfcv 2905 . . . . . . . . . . . . 13 𝑧(2nd ‘(1st𝑝))
29 nfsbc1v 3729 . . . . . . . . . . . . 13 𝑧[(2nd𝑝) / 𝑧]𝜑
3028, 29nfsbcw 3731 . . . . . . . . . . . 12 𝑧[(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3127, 30nfsbcw 3731 . . . . . . . . . . 11 𝑧[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑
3226, 31nfim 1904 . . . . . . . . . 10 𝑧(∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
33 impexp 454 . . . . . . . . . . . . . . . 16 (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
34 elin 3897 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
35 predss 6183 . . . . . . . . . . . . . . . . . . . 20 Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶)
36 sseqin2 4145 . . . . . . . . . . . . . . . . . . . 20 (Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
3735, 36mpbi 233 . . . . . . . . . . . . . . . . . . 19 (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
3837eleq2i 2830 . . . . . . . . . . . . . . . . . 18 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
3934, 38bitr3i 280 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
4039imbi1i 353 . . . . . . . . . . . . . . . 16 (((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
4133, 40bitr3i 280 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)) ↔ (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
4241albii 1827 . . . . . . . . . . . . . 14 (∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)) ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
43 r3al 3124 . . . . . . . . . . . . . . . 16 (∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
44 nfv 1922 . . . . . . . . . . . . . . . . . 18 𝑤 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
45 nfsbc1v 3729 . . . . . . . . . . . . . . . . . 18 𝑤[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
4644, 45nfim 1904 . . . . . . . . . . . . . . . . 17 𝑤(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
47 nfv 1922 . . . . . . . . . . . . . . . . . 18 𝑡 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
48 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑡(1st ‘(1st𝑞))
49 nfsbc1v 3729 . . . . . . . . . . . . . . . . . . 19 𝑡[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5048, 49nfsbcw 3731 . . . . . . . . . . . . . . . . . 18 𝑡[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5147, 50nfim 1904 . . . . . . . . . . . . . . . . 17 𝑡(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
52 nfv 1922 . . . . . . . . . . . . . . . . . 18 𝑢 𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)
53 nfcv 2905 . . . . . . . . . . . . . . . . . . 19 𝑢(1st ‘(1st𝑞))
54 nfcv 2905 . . . . . . . . . . . . . . . . . . . 20 𝑢(2nd ‘(1st𝑞))
55 nfsbc1v 3729 . . . . . . . . . . . . . . . . . . . 20 𝑢[(2nd𝑞) / 𝑢]𝜃
5654, 55nfsbcw 3731 . . . . . . . . . . . . . . . . . . 19 𝑢[(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5753, 56nfsbcw 3731 . . . . . . . . . . . . . . . . . 18 𝑢[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃
5852, 57nfim 1904 . . . . . . . . . . . . . . . . 17 𝑢(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)
59 nfv 1922 . . . . . . . . . . . . . . . . 17 𝑞(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)
60 eleq1 2826 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
61 sbcoteq1a 33429 . . . . . . . . . . . . . . . . . 18 (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → ([(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜃))
6260, 61imbi12d 348 . . . . . . . . . . . . . . . . 17 (𝑞 = ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ → ((𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
6346, 51, 58, 59, 62ralxp3f 33427 . . . . . . . . . . . . . . . 16 (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑤𝐴𝑡𝐵𝑢𝐶 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
64 elin 3897 . . . . . . . . . . . . . . . . . . . . . 22 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)))
6537eleq2i 2830 . . . . . . . . . . . . . . . . . . . . . 22 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ (((𝐴 × 𝐵) × 𝐶) ∩ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6664, 65bitr3i 280 . . . . . . . . . . . . . . . . . . . . 21 ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) ↔ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
6766imbi1i 353 . . . . . . . . . . . . . . . . . . . 20 (((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
68 impexp 454 . . . . . . . . . . . . . . . . . . . 20 (((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
6967, 68bitr3i 280 . . . . . . . . . . . . . . . . . . 19 ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
70 ot2elxp 33421 . . . . . . . . . . . . . . . . . . . 20 (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑤𝐴𝑡𝐵𝑢𝐶))
7170imbi1i 353 . . . . . . . . . . . . . . . . . . 19 ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ ((𝐴 × 𝐵) × 𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
7269, 71bitri 278 . . . . . . . . . . . . . . . . . 18 ((⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
7372albii 1827 . . . . . . . . . . . . . . . . 17 (∀𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
74732albii 1828 . . . . . . . . . . . . . . . 16 (∀𝑤𝑡𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑤𝑡𝑢((𝑤𝐴𝑡𝐵𝑢𝐶) → (⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃)))
7543, 63, 743bitr4ri 307 . . . . . . . . . . . . . . 15 (∀𝑤𝑡𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
76 df-ral 3067 . . . . . . . . . . . . . . 15 (∀𝑞 ∈ ((𝐴 × 𝐵) × 𝐶)(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
7775, 76bitri 278 . . . . . . . . . . . . . 14 (∀𝑤𝑡𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) ↔ ∀𝑞(𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃)))
78 df-ral 3067 . . . . . . . . . . . . . 14 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑞(𝑞 ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → [(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
7942, 77, 783bitr4ri 307 . . . . . . . . . . . . 13 (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑤𝑡𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃))
80 frpoins3xp3g.1 . . . . . . . . . . . . 13 ((𝑥𝐴𝑦𝐵𝑧𝐶) → (∀𝑤𝑡𝑢(⟨⟨𝑤, 𝑡⟩, 𝑢⟩ ∈ Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩) → 𝜃) → 𝜑))
8179, 80syl5bi 245 . . . . . . . . . . . 12 ((𝑥𝐴𝑦𝐵𝑧𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜑))
82 predeq3 6180 . . . . . . . . . . . . . 14 (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝) = Pred(𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩))
8382raleqdv 3338 . . . . . . . . . . . . 13 (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃 ↔ ∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃))
84 sbcoteq1a 33429 . . . . . . . . . . . . 13 (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ([(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑𝜑))
8583, 84imbi12d 348 . . . . . . . . . . . 12 (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → ((∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑) ↔ (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑥, 𝑦⟩, 𝑧⟩)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃𝜑)))
8681, 85syl5ibrcom 250 . . . . . . . . . . 11 ((𝑥𝐴𝑦𝐵𝑧𝐶) → (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
87863expia 1123 . . . . . . . . . 10 ((𝑥𝐴𝑦𝐵) → (𝑧𝐶 → (𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
8825, 32, 87rexlimd 3244 . . . . . . . . 9 ((𝑥𝐴𝑦𝐵) → (∃𝑧𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)))
8988ex 416 . . . . . . . 8 (𝑥𝐴 → (𝑦𝐵 → (∃𝑧𝐶 𝑝 = ⟨⟨𝑥, 𝑦⟩, 𝑧⟩ → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))))
9019, 24, 89rexlimd 3244 . . . . . . 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 220 . . . . 5 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑤][(2nd ‘(1st𝑞)) / 𝑡][(2nd𝑞) / 𝑢]𝜃[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))
9314, 92syl5bi 245 . . . 4 (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → (∀𝑞 ∈ Pred (𝑅, ((𝐴 × 𝐵) × 𝐶), 𝑝)[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑))
94 2fveq3 6741 . . . . 5 (𝑝 = 𝑞 → (1st ‘(1st𝑝)) = (1st ‘(1st𝑞)))
95 2fveq3 6741 . . . . . 6 (𝑝 = 𝑞 → (2nd ‘(1st𝑝)) = (2nd ‘(1st𝑞)))
96 fveq2 6736 . . . . . . 7 (𝑝 = 𝑞 → (2nd𝑝) = (2nd𝑞))
9796sbceq1d 3714 . . . . . 6 (𝑝 = 𝑞 → ([(2nd𝑝) / 𝑧]𝜑[(2nd𝑞) / 𝑧]𝜑))
9895, 97sbceqbid 3716 . . . . 5 (𝑝 = 𝑞 → ([(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
9994, 98sbceqbid 3716 . . . 4 (𝑝 = 𝑞 → ([(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑[(1st ‘(1st𝑞)) / 𝑥][(2nd ‘(1st𝑞)) / 𝑦][(2nd𝑞) / 𝑧]𝜑))
10093, 99frpoins2g 6217 . . 3 ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑)
101 ralxp3es 33430 . . 3 (∀𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)[(1st ‘(1st𝑝)) / 𝑥][(2nd ‘(1st𝑝)) / 𝑦][(2nd𝑝) / 𝑧]𝜑 ↔ ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑)
102100, 101sylib 221 . 2 ((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) → ∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑)
103 frpoins3xp3g.5 . . 3 (𝑥 = 𝑋 → (𝜑𝜏))
104 frpoins3xp3g.6 . . 3 (𝑦 = 𝑌 → (𝜏𝜂))
105 frpoins3xp3g.7 . . 3 (𝑧 = 𝑍 → (𝜂𝜁))
106103, 104, 105rspc3v 3563 . 2 ((𝑋𝐴𝑌𝐵𝑍𝐶) → (∀𝑥𝐴𝑦𝐵𝑧𝐶 𝜑𝜁))
107102, 106mpan9 510 1 (((𝑅 Fr ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Po ((𝐴 × 𝐵) × 𝐶) ∧ 𝑅 Se ((𝐴 × 𝐵) × 𝐶)) ∧ (𝑋𝐴𝑌𝐵𝑍𝐶)) → 𝜁)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1089  wal 1541   = wceq 1543  wcel 2111  wral 3062  wrex 3063  [wsbc 3709  cin 3880  wss 3881  cop 4562   Po wpo 5481   Fr wfr 5521   Se wse 5522   × cxp 5564  Predcpred 6175  cfv 6398  1st c1st 7778  2nd c2nd 7779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5207  ax-nul 5214  ax-pr 5337  ax-un 7542
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3423  df-sbc 3710  df-csb 3827  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-if 4455  df-sn 4557  df-pr 4559  df-op 4563  df-uni 4835  df-iun 4921  df-br 5069  df-opab 5131  df-mpt 5151  df-id 5470  df-po 5483  df-fr 5524  df-se 5525  df-xp 5572  df-rel 5573  df-cnv 5574  df-co 5575  df-dm 5576  df-rn 5577  df-res 5578  df-ima 5579  df-pred 6176  df-iota 6356  df-fun 6400  df-fv 6406  df-1st 7780  df-2nd 7781
This theorem is referenced by:  xpord3ind  33566
  Copyright terms: Public domain W3C validator