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

Theorem xpord3indd 8120
Description: Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025.)
Hypotheses
Ref Expression
xpord3indd.x (𝜅𝑋𝐴)
xpord3indd.y (𝜅𝑌𝐵)
xpord3indd.z (𝜅𝑍𝐶)
xpord3indd.1 (𝜅𝑅 Fr 𝐴)
xpord3indd.2 (𝜅𝑅 Po 𝐴)
xpord3indd.3 (𝜅𝑅 Se 𝐴)
xpord3indd.4 (𝜅𝑆 Fr 𝐵)
xpord3indd.5 (𝜅𝑆 Po 𝐵)
xpord3indd.6 (𝜅𝑆 Se 𝐵)
xpord3indd.7 (𝜅𝑇 Fr 𝐶)
xpord3indd.8 (𝜅𝑇 Po 𝐶)
xpord3indd.9 (𝜅𝑇 Se 𝐶)
xpord3indd.10 (𝑎 = 𝑑 → (𝜑𝜓))
xpord3indd.11 (𝑏 = 𝑒 → (𝜓𝜒))
xpord3indd.12 (𝑐 = 𝑓 → (𝜒𝜃))
xpord3indd.13 (𝑎 = 𝑑 → (𝜏𝜃))
xpord3indd.14 (𝑏 = 𝑒 → (𝜂𝜏))
xpord3indd.15 (𝑏 = 𝑒 → (𝜁𝜃))
xpord3indd.16 (𝑐 = 𝑓 → (𝜎𝜏))
xpord3indd.17 (𝑎 = 𝑋 → (𝜑𝜌))
xpord3indd.18 (𝑏 = 𝑌 → (𝜌𝜇))
xpord3indd.19 (𝑐 = 𝑍 → (𝜇𝜆))
xpord3indd.i ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))
Assertion
Ref Expression
xpord3indd (𝜅𝜆)
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑅,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑆,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑇,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝑋,𝑎,𝑏,𝑐   𝑌,𝑏,𝑐   𝑍,𝑐   𝜅,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓   𝜓,𝑎   𝜌,𝑎   𝜃,𝑎   𝜒,𝑏,𝑓   𝜇,𝑏   𝜃,𝑏   𝜆,𝑐   𝜃,𝑐   𝜑,𝑑   𝜏,𝑑   𝜂,𝑒   𝜓,𝑒   𝜁,𝑒   𝜎,𝑓
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑎,𝑏,𝑐)   𝜓(𝑓,𝑏,𝑐,𝑑)   𝜒(𝑒,𝑎,𝑐,𝑑)   𝜃(𝑒,𝑓,𝑑)   𝜏(𝑒,𝑓,𝑎,𝑏,𝑐)   𝜂(𝑓,𝑎,𝑏,𝑐,𝑑)   𝜁(𝑓,𝑎,𝑏,𝑐,𝑑)   𝜎(𝑒,𝑎,𝑏,𝑐,𝑑)   𝜌(𝑒,𝑓,𝑏,𝑐,𝑑)   𝜇(𝑒,𝑓,𝑎,𝑐,𝑑)   𝜆(𝑒,𝑓,𝑎,𝑏,𝑑)   𝑋(𝑒,𝑓,𝑑)   𝑌(𝑒,𝑓,𝑎,𝑑)   𝑍(𝑒,𝑓,𝑎,𝑏,𝑑)

Proof of Theorem xpord3indd
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2731 . 2 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
2 xpord3indd.x . 2 (𝜅𝑋𝐴)
3 xpord3indd.y . 2 (𝜅𝑌𝐵)
4 xpord3indd.z . 2 (𝜅𝑍𝐶)
5 xpord3indd.1 . 2 (𝜅𝑅 Fr 𝐴)
6 xpord3indd.2 . 2 (𝜅𝑅 Po 𝐴)
7 xpord3indd.3 . 2 (𝜅𝑅 Se 𝐴)
8 xpord3indd.4 . 2 (𝜅𝑆 Fr 𝐵)
9 xpord3indd.5 . 2 (𝜅𝑆 Po 𝐵)
10 xpord3indd.6 . 2 (𝜅𝑆 Se 𝐵)
11 xpord3indd.7 . 2 (𝜅𝑇 Fr 𝐶)
12 xpord3indd.8 . 2 (𝜅𝑇 Po 𝐶)
13 xpord3indd.9 . 2 (𝜅𝑇 Se 𝐶)
14 xpord3indd.10 . 2 (𝑎 = 𝑑 → (𝜑𝜓))
15 xpord3indd.11 . 2 (𝑏 = 𝑒 → (𝜓𝜒))
16 xpord3indd.12 . 2 (𝑐 = 𝑓 → (𝜒𝜃))
17 xpord3indd.13 . 2 (𝑎 = 𝑑 → (𝜏𝜃))
18 xpord3indd.14 . 2 (𝑏 = 𝑒 → (𝜂𝜏))
19 xpord3indd.15 . 2 (𝑏 = 𝑒 → (𝜁𝜃))
20 xpord3indd.16 . 2 (𝑐 = 𝑓 → (𝜎𝜏))
21 xpord3indd.17 . 2 (𝑎 = 𝑋 → (𝜑𝜌))
22 xpord3indd.18 . 2 (𝑏 = 𝑌 → (𝜌𝜇))
23 xpord3indd.19 . 2 (𝑐 = 𝑍 → (𝜇𝜆))
24 xpord3indd.i . 2 ((𝜅 ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) → (((∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜃 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜁) ∧ (∀𝑑 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜏 ∧ ∀𝑒 ∈ Pred (𝑆, 𝐵, 𝑏)𝜎) ∧ ∀𝑓 ∈ Pred (𝑇, 𝐶, 𝑐)𝜂) → 𝜑))
251, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24xpord3inddlem 8119 1 (𝜅𝜆)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087   = wceq 1541  wcel 2106  wne 2939  wral 3060   class class class wbr 5138  {copab 5200   Po wpo 5576   Fr wfr 5618   Se wse 5619   × cxp 5664  Predcpred 6285  cfv 6529  1st c1st 7952  2nd c2nd 7953
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 2702  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7705
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  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 3430  df-v 3472  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4520  df-pw 4595  df-sn 4620  df-pr 4622  df-op 4626  df-ot 4628  df-uni 4899  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-po 5578  df-fr 5621  df-se 5622  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6286  df-iota 6481  df-fun 6531  df-fv 6537  df-1st 7954  df-2nd 7955
This theorem is referenced by:  xpord3ind  8121
  Copyright terms: Public domain W3C validator