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

Theorem oi0 9566
Description: Definition of the ordinal isomorphism when its arguments are not meaningful. (Contributed by Mario Carneiro, 25-Jun-2015.)
Hypothesis
Ref Expression
oicl.1 𝐹 = OrdIso(𝑅, 𝐴)
Assertion
Ref Expression
oi0 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹 = ∅)

Proof of Theorem oi0
Dummy variables 𝑢 𝑡 𝑣 𝑥 𝑗 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oicl.1 . . 3 𝐹 = OrdIso(𝑅, 𝐴)
2 df-oi 9548 . . 3 OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
31, 2eqtri 2763 . 2 𝐹 = if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅)
4 iffalse 4540 . 2 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑥)𝑧𝑅𝑡}), ∅) = ∅)
53, 4eqtrid 2787 1 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1537  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  c0 4339  ifcif 4531   class class class wbr 5148  cmpt 5231   Se wse 5639   We wwe 5640  ran crn 5690  cres 5691  cima 5692  Oncon0 6386  crio 7387  recscrecs 8409  OrdIsocoi 9547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532  df-oi 9548
This theorem is referenced by:  oicl  9567  oif  9568  oiexg  9573
  Copyright terms: Public domain W3C validator