ordtypelem9

Description: Lemma for ordtype . Either the function OrdIso is an isomorphism onto all of A , or OrdIso is not a set, which by oif implies that either ran O C_ A is a proper class or dom O = On . (Contributed by Mario Carneiro, 25-Jun-2015) (Revised by AV, 28-Jul-2024)

	Ref	Expression
Hypotheses	ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
	ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
	ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
	ordtypelem.5	⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
	ordtypelem.6	⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
	ordtypelem.7	⊢ ( 𝜑 → 𝑅 We 𝐴 )
	ordtypelem.8	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
	ordtypelem9.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
Assertion	ordtypelem9	⊢ ( 𝜑 → 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtypelem.1	⊢ 𝐹 = recs ( 𝐺 )
2		ordtypelem.2	⊢ 𝐶 = { 𝑤 ∈ 𝐴 ∣ ∀ 𝑗 ∈ ran ℎ 𝑗 𝑅 𝑤 }
3		ordtypelem.3	⊢ 𝐺 = ( ℎ ∈ V ↦ ( ℩ 𝑣 ∈ 𝐶 ∀ 𝑢 ∈ 𝐶 ¬ 𝑢 𝑅 𝑣 ) )
4		ordtypelem.5	⊢ 𝑇 = { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 }
5		ordtypelem.6	⊢ 𝑂 = OrdIso ( 𝑅 , 𝐴 )
6		ordtypelem.7	⊢ ( 𝜑 → 𝑅 We 𝐴 )
7		ordtypelem.8	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
8		ordtypelem9.1	⊢ ( 𝜑 → 𝑂 ∈ 𝑉 )
9	1 2 3 4 5 6 7	ordtypelem8	⊢ ( 𝜑 → 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) )
10	1 2 3 4 5 6 7	ordtypelem4	⊢ ( 𝜑 → 𝑂 : ( 𝑇 ∩ dom 𝐹 ) ⟶ 𝐴 )
11	10	frnd	⊢ ( 𝜑 → ran 𝑂 ⊆ 𝐴 )
12	1 2 3 4 5 6 7	ordtypelem2	⊢ ( 𝜑 → Ord 𝑇 )
13		ordirr	⊢ ( Ord 𝑇 → ¬ 𝑇 ∈ 𝑇 )
14	12 13	syl	⊢ ( 𝜑 → ¬ 𝑇 ∈ 𝑇 )
15	1	tfr1a	⊢ ( Fun 𝐹 ∧ Lim dom 𝐹 )
16	15	simpri	⊢ Lim dom 𝐹
17		limord	⊢ ( Lim dom 𝐹 → Ord dom 𝐹 )
18	16 17	ax-mp	⊢ Ord dom 𝐹
19	1 2 3 4 5 6 7	ordtypelem1	⊢ ( 𝜑 → 𝑂 = ( 𝐹 ↾ 𝑇 ) )
20	8	elexd	⊢ ( 𝜑 → 𝑂 ∈ V )
21	19 20	eqeltrrd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝑇 ) ∈ V )
22	1	tfr2b	⊢ ( Ord 𝑇 → ( 𝑇 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝑇 ) ∈ V ) )
23	12 22	syl	⊢ ( 𝜑 → ( 𝑇 ∈ dom 𝐹 ↔ ( 𝐹 ↾ 𝑇 ) ∈ V ) )
24	21 23	mpbird	⊢ ( 𝜑 → 𝑇 ∈ dom 𝐹 )
25		ordelon	⊢ ( ( Ord dom 𝐹 ∧ 𝑇 ∈ dom 𝐹 ) → 𝑇 ∈ On )
26	18 24 25	sylancr	⊢ ( 𝜑 → 𝑇 ∈ On )
27		imaeq2	⊢ ( 𝑎 = 𝑇 → ( 𝐹 “ 𝑎 ) = ( 𝐹 “ 𝑇 ) )
28	27	raleqdv	⊢ ( 𝑎 = 𝑇 → ( ∀ 𝑐 ∈ ( 𝐹 “ 𝑎 ) 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ) )
29	28	rexbidv	⊢ ( 𝑎 = 𝑇 → ( ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑎 ) 𝑐 𝑅 𝑏 ↔ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ) )
30		breq1	⊢ ( 𝑧 = 𝑐 → ( 𝑧 𝑅 𝑡 ↔ 𝑐 𝑅 𝑡 ) )
31	30	cbvralvw	⊢ ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑐 ∈ ( 𝐹 “ 𝑥 ) 𝑐 𝑅 𝑡 )
32		breq2	⊢ ( 𝑡 = 𝑏 → ( 𝑐 𝑅 𝑡 ↔ 𝑐 𝑅 𝑏 ) )
33	32	ralbidv	⊢ ( 𝑡 = 𝑏 → ( ∀ 𝑐 ∈ ( 𝐹 “ 𝑥 ) 𝑐 𝑅 𝑡 ↔ ∀ 𝑐 ∈ ( 𝐹 “ 𝑥 ) 𝑐 𝑅 𝑏 ) )
34	31 33	bitrid	⊢ ( 𝑡 = 𝑏 → ( ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∀ 𝑐 ∈ ( 𝐹 “ 𝑥 ) 𝑐 𝑅 𝑏 ) )
35	34	cbvrexvw	⊢ ( ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑥 ) 𝑐 𝑅 𝑏 )
36		imaeq2	⊢ ( 𝑥 = 𝑎 → ( 𝐹 “ 𝑥 ) = ( 𝐹 “ 𝑎 ) )
37	36	raleqdv	⊢ ( 𝑥 = 𝑎 → ( ∀ 𝑐 ∈ ( 𝐹 “ 𝑥 ) 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ ( 𝐹 “ 𝑎 ) 𝑐 𝑅 𝑏 ) )
38	37	rexbidv	⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑥 ) 𝑐 𝑅 𝑏 ↔ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑎 ) 𝑐 𝑅 𝑏 ) )
39	35 38	bitrid	⊢ ( 𝑥 = 𝑎 → ( ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 ↔ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑎 ) 𝑐 𝑅 𝑏 ) )
40	39	cbvrabv	⊢ { 𝑥 ∈ On ∣ ∃ 𝑡 ∈ 𝐴 ∀ 𝑧 ∈ ( 𝐹 “ 𝑥 ) 𝑧 𝑅 𝑡 } = { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑎 ) 𝑐 𝑅 𝑏 }
41	4 40	eqtri	⊢ 𝑇 = { 𝑎 ∈ On ∣ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑎 ) 𝑐 𝑅 𝑏 }
42	29 41	elrab2	⊢ ( 𝑇 ∈ 𝑇 ↔ ( 𝑇 ∈ On ∧ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ) )
43	42	baib	⊢ ( 𝑇 ∈ On → ( 𝑇 ∈ 𝑇 ↔ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ) )
44	26 43	syl	⊢ ( 𝜑 → ( 𝑇 ∈ 𝑇 ↔ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ) )
45	14 44	mtbid	⊢ ( 𝜑 → ¬ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 )
46		ralnex	⊢ ( ∀ 𝑏 ∈ 𝐴 ¬ ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ↔ ¬ ∃ 𝑏 ∈ 𝐴 ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 )
47	45 46	sylibr	⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐴 ¬ ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 )
48	47	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ¬ ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 )
49	19	rneqd	⊢ ( 𝜑 → ran 𝑂 = ran ( 𝐹 ↾ 𝑇 ) )
50		df-ima	⊢ ( 𝐹 “ 𝑇 ) = ran ( 𝐹 ↾ 𝑇 )
51	49 50	eqtr4di	⊢ ( 𝜑 → ran 𝑂 = ( 𝐹 “ 𝑇 ) )
52	51	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ran 𝑂 = ( 𝐹 “ 𝑇 ) )
53	52	raleqdv	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ) )
54	10	ffund	⊢ ( 𝜑 → Fun 𝑂 )
55	54	funfnd	⊢ ( 𝜑 → 𝑂 Fn dom 𝑂 )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝑂 Fn dom 𝑂 )
57		breq1	⊢ ( 𝑐 = ( 𝑂 ‘ 𝑚 ) → ( 𝑐 𝑅 𝑏 ↔ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
58	57	ralrn	⊢ ( 𝑂 Fn dom 𝑂 → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
59	56 58	syl	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑐 ∈ ran 𝑂 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
60	53 59	bitr3d	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑐 ∈ ( 𝐹 “ 𝑇 ) 𝑐 𝑅 𝑏 ↔ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ) )
61	48 60	mtbid	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ¬ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 )
62		rexnal	⊢ ( ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ↔ ¬ ∀ 𝑚 ∈ dom 𝑂 ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 )
63	61 62	sylibr	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 )
64	1 2 3 4 5 6 7	ordtypelem7	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑚 ∈ dom 𝑂 ) → ( ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 ∨ 𝑏 ∈ ran 𝑂 ) )
65	64	ord	⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) ∧ 𝑚 ∈ dom 𝑂 ) → ( ¬ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 → 𝑏 ∈ ran 𝑂 ) )
66	65	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → ( ∃ 𝑚 ∈ dom 𝑂 ¬ ( 𝑂 ‘ 𝑚 ) 𝑅 𝑏 → 𝑏 ∈ ran 𝑂 ) )
67	63 66	mpd	⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ ran 𝑂 )
68	11 67	eqelssd	⊢ ( 𝜑 → ran 𝑂 = 𝐴 )
69		isoeq5	⊢ ( ran 𝑂 = 𝐴 → ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) ↔ 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) ) )
70	68 69	syl	⊢ ( 𝜑 → ( 𝑂 Isom E , 𝑅 ( dom 𝑂 , ran 𝑂 ) ↔ 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) ) )
71	9 70	mpbid	⊢ ( 𝜑 → 𝑂 Isom E , 𝑅 ( dom 𝑂 , 𝐴 ) )

Metamath Proof Explorer

Theorem ordtypelem9

Proof