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

Theorem xpord3lem 33398
Description: Lemma for triple ordering. Calculate the value of the relationship. (Contributed by Scott Fenton, 21-Aug-2024.)
Hypothesis
Ref Expression
xpord3.1 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
Assertion
Ref Expression
xpord3lem (⟨⟨𝑎, 𝑏⟩, 𝑐𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ (𝑎𝑑𝑏𝑒𝑐𝑓))))
Distinct variable groups:   𝑥,𝑎   𝑥,𝐴   𝑦,𝑎   𝑦,𝐴   𝑥,𝑏   𝑥,𝐵   𝑦,𝑏   𝑦,𝐵   𝑥,𝑐   𝑥,𝐶   𝑦,𝑐   𝑦,𝐶   𝑥,𝑑,𝑦   𝑥,𝑒,𝑦   𝑥,𝑓,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦
Allowed substitution hints:   𝐴(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝐵(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝐶(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑅(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑆(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑇(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑈(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem xpord3lem
StepHypRef Expression
1 opex 5319 . . 3 ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ V
2 opex 5319 . . 3 ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ V
3 eleq1 2820 . . . 4 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4 vex 3401 . . . . . . . . 9 𝑎 ∈ V
5 vex 3401 . . . . . . . . 9 𝑏 ∈ V
6 vex 3401 . . . . . . . . 9 𝑐 ∈ V
74, 5, 6ot21std 33246 . . . . . . . 8 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (1st ‘(1st𝑥)) = 𝑎)
87breq1d 5037 . . . . . . 7 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ↔ 𝑎𝑅(1st ‘(1st𝑦))))
97eqeq1d 2740 . . . . . . 7 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((1st ‘(1st𝑥)) = (1st ‘(1st𝑦)) ↔ 𝑎 = (1st ‘(1st𝑦))))
108, 9orbi12d 918 . . . . . 6 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ↔ (𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦)))))
114, 5, 6ot22ndd 33247 . . . . . . . 8 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (2nd ‘(1st𝑥)) = 𝑏)
1211breq1d 5037 . . . . . . 7 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ↔ 𝑏𝑆(2nd ‘(1st𝑦))))
1311eqeq1d 2740 . . . . . . 7 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦)) ↔ 𝑏 = (2nd ‘(1st𝑦))))
1412, 13orbi12d 918 . . . . . 6 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ↔ (𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦)))))
15 opex 5319 . . . . . . . . 9 𝑎, 𝑏⟩ ∈ V
1615, 6op2ndd 7718 . . . . . . . 8 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (2nd𝑥) = 𝑐)
1716breq1d 5037 . . . . . . 7 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd𝑥)𝑇(2nd𝑦) ↔ 𝑐𝑇(2nd𝑦)))
1816eqeq1d 2740 . . . . . . 7 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd𝑥) = (2nd𝑦) ↔ 𝑐 = (2nd𝑦)))
1917, 18orbi12d 918 . . . . . 6 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ↔ (𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦))))
2010, 14, 193anbi123d 1437 . . . . 5 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ↔ ((𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦))) ∧ (𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦))) ∧ (𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦)))))
21 neeq1 2996 . . . . 5 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑥𝑦 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦))
2220, 21anbi12d 634 . . . 4 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦) ↔ (((𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦))) ∧ (𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦))) ∧ (𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦)))
233, 223anbi13d 1439 . . 3 (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦)) ↔ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦))) ∧ (𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦))) ∧ (𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦))))
24 eleq1 2820 . . . 4 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
25 vex 3401 . . . . . . . . 9 𝑑 ∈ V
26 vex 3401 . . . . . . . . 9 𝑒 ∈ V
27 vex 3401 . . . . . . . . 9 𝑓 ∈ V
2825, 26, 27ot21std 33246 . . . . . . . 8 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (1st ‘(1st𝑦)) = 𝑑)
2928breq2d 5039 . . . . . . 7 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑅(1st ‘(1st𝑦)) ↔ 𝑎𝑅𝑑))
3028eqeq2d 2749 . . . . . . 7 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎 = (1st ‘(1st𝑦)) ↔ 𝑎 = 𝑑))
3129, 30orbi12d 918 . . . . . 6 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦))) ↔ (𝑎𝑅𝑑𝑎 = 𝑑)))
3225, 26, 27ot22ndd 33247 . . . . . . . 8 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (2nd ‘(1st𝑦)) = 𝑒)
3332breq2d 5039 . . . . . . 7 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st𝑦)) ↔ 𝑏𝑆𝑒))
3432eqeq2d 2749 . . . . . . 7 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑏 = (2nd ‘(1st𝑦)) ↔ 𝑏 = 𝑒))
3533, 34orbi12d 918 . . . . . 6 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦))) ↔ (𝑏𝑆𝑒𝑏 = 𝑒)))
36 opex 5319 . . . . . . . . 9 𝑑, 𝑒⟩ ∈ V
3736, 27op2ndd 7718 . . . . . . . 8 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (2nd𝑦) = 𝑓)
3837breq2d 5039 . . . . . . 7 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑐𝑇(2nd𝑦) ↔ 𝑐𝑇𝑓))
3937eqeq2d 2749 . . . . . . 7 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑐 = (2nd𝑦) ↔ 𝑐 = 𝑓))
4038, 39orbi12d 918 . . . . . 6 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦)) ↔ (𝑐𝑇𝑓𝑐 = 𝑓)))
4131, 35, 403anbi123d 1437 . . . . 5 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦))) ∧ (𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦))) ∧ (𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦))) ↔ ((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓))))
42 neeq2 2997 . . . . 5 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
4341, 42anbi12d 634 . . . 4 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦))) ∧ (𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦))) ∧ (𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)))
4424, 433anbi23d 1440 . . 3 (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st𝑦)) ∨ 𝑎 = (1st ‘(1st𝑦))) ∧ (𝑏𝑆(2nd ‘(1st𝑦)) ∨ 𝑏 = (2nd ‘(1st𝑦))) ∧ (𝑐𝑇(2nd𝑦) ∨ 𝑐 = (2nd𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦)) ↔ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩))))
45 xpord3.1 . . 3 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
461, 2, 23, 44, 45brab 5395 . 2 (⟨⟨𝑎, 𝑏⟩, 𝑐𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)))
47 ot2elxp 33245 . . 3 (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎𝐴𝑏𝐵𝑐𝐶))
48 ot2elxp 33245 . . 3 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑𝐴𝑒𝐵𝑓𝐶))
494, 5, 6otthne 33248 . . . 4 (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ (𝑎𝑑𝑏𝑒𝑐𝑓))
5049anbi2i 626 . . 3 ((((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩) ↔ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ (𝑎𝑑𝑏𝑒𝑐𝑓)))
5147, 48, 503anbi123i 1156 . 2 ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)) ↔ ((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ (𝑎𝑑𝑏𝑒𝑐𝑓))))
5246, 51bitri 278 1 (⟨⟨𝑎, 𝑏⟩, 𝑐𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (((𝑎𝑅𝑑𝑎 = 𝑑) ∧ (𝑏𝑆𝑒𝑏 = 𝑒) ∧ (𝑐𝑇𝑓𝑐 = 𝑓)) ∧ (𝑎𝑑𝑏𝑒𝑐𝑓))))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wo 846  w3o 1087  w3a 1088   = wceq 1542  wcel 2113  wne 2934  cop 4519   class class class wbr 5027  {copab 5089   × cxp 5517  cfv 6333  1st c1st 7705  2nd c2nd 7706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-sbc 3680  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6291  df-fun 6335  df-fv 6341  df-1st 7707  df-2nd 7708
This theorem is referenced by:  poxp3  33399  frxp3  33400  xpord3pred  33401
  Copyright terms: Public domain W3C validator