Metamath Proof Explorer


Theorem oicl

Description: The order type of the well-order R on A is an ordinal. (Contributed by Mario Carneiro, 23-May-2015) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Hypothesis oicl.1 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion oicl Ord dom 𝐹

Proof

Step Hyp Ref Expression
1 oicl.1 𝐹 = OrdIso ( 𝑅 , 𝐴 )
2 eqid recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) ) = recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) )
3 eqid { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } = { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 }
4 eqid ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) = ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) )
5 2 3 4 ordtypecbv recs ( ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) = recs ( ( ∈ V ↦ ( 𝑣 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ∀ 𝑢 ∈ { 𝑤𝐴 ∣ ∀ 𝑗 ∈ ran 𝑗 𝑅 𝑤 } ¬ 𝑢 𝑅 𝑣 ) ) )
6 eqid { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 } = { 𝑥 ∈ On ∣ ∃ 𝑡𝐴𝑧 ∈ ( recs ( ( 𝑓 ∈ V ↦ ( 𝑠 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ∀ 𝑟 ∈ { 𝑦𝐴 ∣ ∀ 𝑖 ∈ ran 𝑓 𝑖 𝑅 𝑦 } ¬ 𝑟 𝑅 𝑠 ) ) ) “ 𝑥 ) 𝑧 𝑅 𝑡 }
7 simpl ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → 𝑅 We 𝐴 )
8 simpr ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → 𝑅 Se 𝐴 )
9 5 3 4 6 1 7 8 ordtypelem5 ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → ( Ord dom 𝐹𝐹 : dom 𝐹𝐴 ) )
10 9 simpld ( ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → Ord dom 𝐹 )
11 ord0 Ord ∅
12 1 oi0 ( ¬ ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → 𝐹 = ∅ )
13 12 dmeqd ( ¬ ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → dom 𝐹 = dom ∅ )
14 dm0 dom ∅ = ∅
15 13 14 eqtrdi ( ¬ ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → dom 𝐹 = ∅ )
16 ordeq ( dom 𝐹 = ∅ → ( Ord dom 𝐹 ↔ Ord ∅ ) )
17 15 16 syl ( ¬ ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → ( Ord dom 𝐹 ↔ Ord ∅ ) )
18 11 17 mpbiri ( ¬ ( 𝑅 We 𝐴𝑅 Se 𝐴 ) → Ord dom 𝐹 )
19 10 18 pm2.61i Ord dom 𝐹