This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oif

Description: The order isomorphism of the well-order R on A is a function. (Contributed by Mario Carneiro, 23-May-2015)

Ref Expression
Hypothesis oicl.1 ⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion oif 𝐹 : 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 simprd ⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 : dom 𝐹 ⟶ 𝐴 )
11 f0 ⊢ ∅ : ∅ ⟶ 𝐴
12 1 oi0 ⊢ ( ¬ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 = ∅ )
13 12 dmeqd ⊢ ( ¬ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → dom 𝐹 = dom ∅ )
14 dm0 ⊢ dom ∅ = ∅
15 13 14 eqtrdi ⊢ ( ¬ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → dom 𝐹 = ∅ )
16 12 15 feq12d ⊢ ( ¬ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → ( 𝐹 : dom 𝐹 ⟶ 𝐴 ↔ ∅ : ∅ ⟶ 𝐴 ) )
17 11 16 mpbiri ⊢ ( ¬ ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 : dom 𝐹 ⟶ 𝐴 )
18 10 17 pm2.61i ⊢ 𝐹 : dom 𝐹 ⟶ 𝐴