Theorem ordtype2

Description: For any set-like well-ordered class, if the order isomorphism exists (is a set), then it maps some ordinal onto A isomorphically. Otherwise, F is a proper class, which implies that either ran F C_ A is a proper class or dom F = On . This weak version of ordtype does not require the Axiom of Replacement. (Contributed by Mario Carneiro, 25-Jun-2015)

	Ref	Expression
Hypothesis	oicl.1	⊢ 𝐹 = OrdIso ( 𝑅 , 𝐴 )
Assertion	ordtype2	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V ) → 𝐹 Isom E , 𝑅 ( 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		simp1	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V ) → 𝑅 We 𝐴 )
8		simp2	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V ) → 𝑅 Se 𝐴 )
9		simp3	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V ) → 𝐹 ∈ V )
10	5 3 4 6 1 7 8 9	ordtypelem9	⊢ ( ( 𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐹 ∈ V ) → 𝐹 Isom E , 𝑅 ( dom 𝐹 , 𝐴 ) )