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

Theorem nfoi 8771
 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 8767 . 2 OrdIso(𝑅, 𝐴) = if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}), ∅)
2 nfoi.1 . . . . 5 𝑥𝑅
3 nfoi.2 . . . . 5 𝑥𝐴
42, 3nfwe 5379 . . . 4 𝑥 𝑅 We 𝐴
52, 3nfse 5378 . . . 4 𝑥 𝑅 Se 𝐴
64, 5nfan 1862 . . 3 𝑥(𝑅 We 𝐴𝑅 Se 𝐴)
7 nfcv 2926 . . . . . 6 𝑥V
8 nfcv 2926 . . . . . . . . . 10 𝑥ran
9 nfcv 2926 . . . . . . . . . . 11 𝑥𝑗
10 nfcv 2926 . . . . . . . . . . 11 𝑥𝑤
119, 2, 10nfbr 4972 . . . . . . . . . 10 𝑥 𝑗𝑅𝑤
128, 11nfral 3168 . . . . . . . . 9 𝑥𝑗 ∈ ran 𝑗𝑅𝑤
1312, 3nfrab 3319 . . . . . . . 8 𝑥{𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
14 nfcv 2926 . . . . . . . . . 10 𝑥𝑢
15 nfcv 2926 . . . . . . . . . 10 𝑥𝑣
1614, 2, 15nfbr 4972 . . . . . . . . 9 𝑥 𝑢𝑅𝑣
1716nfn 1819 . . . . . . . 8 𝑥 ¬ 𝑢𝑅𝑣
1813, 17nfral 3168 . . . . . . 7 𝑥𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣
1918, 13nfriota 6944 . . . . . 6 𝑥(𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
207, 19nfmpt 5020 . . . . 5 𝑥( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
2120nfrecs 7813 . . . 4 𝑥recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
22 nfcv 2926 . . . . . . . 8 𝑥𝑎
2321, 22nfima 5775 . . . . . . 7 𝑥(recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)
24 nfcv 2926 . . . . . . . 8 𝑥𝑧
25 nfcv 2926 . . . . . . . 8 𝑥𝑡
2624, 2, 25nfbr 4972 . . . . . . 7 𝑥 𝑧𝑅𝑡
2723, 26nfral 3168 . . . . . 6 𝑥𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡
283, 27nfrex 3247 . . . . 5 𝑥𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡
29 nfcv 2926 . . . . 5 𝑥On
3028, 29nfrab 3319 . . . 4 𝑥{𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}
3121, 30nfres 5694 . . 3 𝑥(recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡})
32 nfcv 2926 . . 3 𝑥
336, 31, 32nfif 4373 . 2 𝑥if((𝑅 We 𝐴𝑅 Se 𝐴), (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) ↾ {𝑎 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) “ 𝑎)𝑧𝑅𝑡}), ∅)
341, 33nfcxfr 2924 1 𝑥OrdIso(𝑅, 𝐴)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 387  Ⅎwnfc 2910  ∀wral 3082  ∃wrex 3083  {crab 3086  Vcvv 3409  ∅c0 4172  ifcif 4344   class class class wbr 4925   ↦ cmpt 5004   Se wse 5360   We wwe 5361  ran crn 5404   ↾ cres 5405   “ cima 5406  Oncon0 6026  ℩crio 6934  recscrecs 7809  OrdIsocoi 8766 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-mpt 5005  df-po 5322  df-so 5323  df-fr 5362  df-se 5363  df-we 5364  df-xp 5409  df-cnv 5411  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-iota 6149  df-fv 6193  df-riota 6935  df-wrecs 7748  df-recs 7810  df-oi 8767 This theorem is referenced by:  hsmexlem2  9645
 Copyright terms: Public domain W3C validator