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

Theorem nfoi 9553
Description: Hypothesis builder for ordinal isomorphism. (Contributed by Mario Carneiro, 23-May-2015.) (Revised by Mario Carneiro, 15-Oct-2016.)
Hypotheses
Ref Expression
nfoi.1 𝑥𝑅
nfoi.2 𝑥𝐴
Assertion
Ref Expression
nfoi 𝑥OrdIso(𝑅, 𝐴)

Proof of Theorem nfoi
Dummy variables 𝑎 𝑗 𝑡 𝑢 𝑣 𝑤 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-oi 9549 . 2 OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}), ∅)
2 nfoi.1 . . . . 5 𝑥𝑅
3 nfoi.2 . . . . 5 𝑥𝐴
42, 3nfwe 5657 . . . 4 𝑥 𝑅 We 𝐴
52, 3nfse 5656 . . . 4 𝑥 𝑅 Se 𝐴
64, 5nfan 1894 . . 3 𝑥(𝑅 We 𝐴𝑅 Se 𝐴)
7 nfcv 2891 . . . . . 6 𝑥V
8 nfcv 2891 . . . . . . . . . 10 𝑥ran
9 nfcv 2891 . . . . . . . . . . 11 𝑥𝑗
10 nfcv 2891 . . . . . . . . . . 11 𝑥𝑤
119, 2, 10nfbr 5199 . . . . . . . . . 10 𝑥 𝑗𝑅𝑤
128, 11nfralw 3298 . . . . . . . . 9 𝑥𝑗 ∈ ran 𝑗𝑅𝑤
1312, 3nfrabw 3456 . . . . . . . 8 𝑥{𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
14 nfcv 2891 . . . . . . . . . 10 𝑥𝑢
15 nfcv 2891 . . . . . . . . . 10 𝑥𝑣
1614, 2, 15nfbr 5199 . . . . . . . . 9 𝑥 𝑢𝑅𝑣
1716nfn 1852 . . . . . . . 8 𝑥 ¬ 𝑢𝑅𝑣
1813, 17nfralw 3298 . . . . . . 7 𝑥𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣
1918, 13nfriota 7392 . . . . . 6 𝑥(𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
207, 19nfmpt 5259 . . . . 5 𝑥( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
2120nfrecs 8404 . . . 4 𝑥recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
22 nfcv 2891 . . . . . . . 8 𝑥𝑎
2321, 22nfima 6076 . . . . . . 7 𝑥(recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)
24 nfcv 2891 . . . . . . . 8 𝑥𝑧
25 nfcv 2891 . . . . . . . 8 𝑥𝑡
2624, 2, 25nfbr 5199 . . . . . . 7 𝑥 𝑧𝑅𝑡
2723, 26nfralw 3298 . . . . . 6 𝑥𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡
283, 27nfrexw 3300 . . . . 5 𝑥𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡
29 nfcv 2891 . . . . 5 𝑥On
3028, 29nfrabw 3456 . . . 4 𝑥{𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}
3121, 30nfres 5990 . . 3 𝑥(recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡})
32 nfcv 2891 . . 3 𝑥
336, 31, 32nfif 4562 . 2 𝑥if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}), ∅)
341, 33nfcxfr 2889 1 𝑥OrdIso(𝑅, 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 394  wnfc 2875  wral 3050  wrex 3059  {crab 3418  Vcvv 3461  c0 4324  ifcif 4532   class class class wbr 5152  cmpt 5235   Se wse 5634   We wwe 5635  ran crn 5682  cres 5683  cima 5684  Oncon0 6375  crio 7378  recscrecs 8399  OrdIsocoi 9548
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4325  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-po 5593  df-so 5594  df-fr 5636  df-se 5637  df-we 5638  df-xp 5687  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-iota 6505  df-fv 6561  df-riota 7379  df-ov 7426  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-oi 9549
This theorem is referenced by:  hsmexlem2  10466
  Copyright terms: Public domain W3C validator