Theorem ordtypelem7 9429

Description: Lemma for ordtype 9437. ran 𝑂 is an initial segment of 𝐴 under the well-order 𝑅. (Contributed by Mario Carneiro, 25-Jun-2015.)

Hypotheses

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

Assertion

Ref	Expression
ordtypelem7	⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂))

Distinct variable groups:   𝑣,𝑢,𝐶   ℎ,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧,𝑀   𝑗,𝑁,𝑢,𝑤   𝑅,ℎ,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧   𝐴,ℎ,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧   𝑡,𝑂,𝑢,𝑣,𝑥   𝜑,𝑡,𝑥   ℎ,𝐹,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧

Allowed substitution hints:   𝜑(𝑧,𝑤,𝑣,𝑢,ℎ,𝑗)   𝐶(𝑥,𝑧,𝑤,𝑡,ℎ,𝑗)   𝑇(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,ℎ,𝑗)   𝐺(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,ℎ,𝑗)   𝑁(𝑥,𝑧,𝑣,𝑡,ℎ)   𝑂(𝑧,𝑤,ℎ,𝑗)

Proof of Theorem ordtypelem7

Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldif 3911	. . . . . 6 ⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) ↔ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂))
2		ordtypelem.1	. . . . . . . . . . . 12 ⊢ 𝐹 = recs(𝐺)
3		ordtypelem.2	. . . . . . . . . . . 12 ⊢ 𝐶 = {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ ran ℎ 𝑗𝑅𝑤}
4		ordtypelem.3	. . . . . . . . . . . 12 ⊢ 𝐺 = (ℎ ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑅𝑣))
5		ordtypelem.5	. . . . . . . . . . . 12 ⊢ 𝑇 = {𝑥 ∈ On ∣ ∃𝑡 ∈ 𝐴 ∀𝑧 ∈ (𝐹 “ 𝑥)𝑧𝑅𝑡}
6		ordtypelem.6	. . . . . . . . . . . 12 ⊢ 𝑂 = OrdIso(𝑅, 𝐴)
7		ordtypelem.7	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 We 𝐴)
8		ordtypelem.8	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 Se 𝐴)
9	2, 3, 4, 5, 6, 7, 8	ordtypelem4 9426	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
10	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
11	10	fdmd 6672	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
12		inss1 4189	. . . . . . . . . 10 ⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇
13	2, 3, 4, 5, 6, 7, 8	ordtypelem2 9424	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝑇)
14	13	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇)
15		ordsson 7728	. . . . . . . . . . 11 ⊢ (Ord 𝑇 → 𝑇 ⊆ On)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On)
17	12, 16	sstrid 3945	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On)
18	11, 17	eqsstrd 3968	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On)
19	18	sseld 3932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → 𝑀 ∈ On))
20		eleq1 2824	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂 ↔ 𝑏 ∈ dom 𝑂))
21		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (𝑂‘𝑎) = (𝑂‘𝑏))
22	21	breq1d 5108	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑏)𝑅𝑁))
23	20, 22	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))
24	23	imbi2d 340	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))))
25		eleq1 2824	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂 ↔ 𝑀 ∈ dom 𝑂))
26		fveq2 6834	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑀 → (𝑂‘𝑎) = (𝑂‘𝑀))
27	26	breq1d 5108	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑀 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑀)𝑅𝑁))
28	25, 27	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))
29	28	imbi2d 340	. . . . . . . . 9 ⊢ (𝑎 = 𝑀 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))))
30		r19.21v 3161	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ 𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))
31	2	tfr1a 8325	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐹 ∧ Lim dom 𝐹)
32	31	simpri 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Lim dom 𝐹
33		limord 6378	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Lim dom 𝐹 → Ord dom 𝐹)
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐹
35		ordin 6347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹))
36	14, 34, 35	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹))
37		ordeq 6324	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (dom 𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
38	11, 37	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
39	36, 38	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂)
40		ordelss 6333	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord dom 𝑂 ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
41	39, 40	sylan 580	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
42	41	sselda 3933	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ dom 𝑂)
43		pm5.5 361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁))
44	42, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁))
45	44	ralbidva 3157	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁))
46		eldifn 4084	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂)
47	46	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂)
48	9	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
49	48	ffnd 6663	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹))
50		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂)
51	48	fdmd 6672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
52	50, 51	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹))
53		fnfvelrn 7025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂‘𝑎) ∈ ran 𝑂)
54	49, 52, 53	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ ran 𝑂)
55		eleq1 2824	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑂‘𝑎) = 𝑁 → ((𝑂‘𝑎) ∈ ran 𝑂 ↔ 𝑁 ∈ ran 𝑂))
56	54, 55	syl5ibcom 245	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎) = 𝑁 → 𝑁 ∈ ran 𝑂))
57	47, 56	mtod 198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ (𝑂‘𝑎) = 𝑁)
58		breq1 5101	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑁 → (𝑢𝑅(𝑂‘𝑎) ↔ 𝑁𝑅(𝑂‘𝑎)))
59	58	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂‘𝑎) ↔ ¬ 𝑁𝑅(𝑂‘𝑎)))
60	2, 3, 4, 5, 6, 7, 8	ordtypelem1 9423	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇))
61	60	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 = (𝐹 ↾ 𝑇))
62	61	fveq1d 6836	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = ((𝐹 ↾ 𝑇)‘𝑎))
63	52	elin1d 4156	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ 𝑇)
64	63	fvresd 6854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎))
65	62, 64	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = (𝐹‘𝑎))
66		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝜑)
67	2, 3, 4, 5, 6, 7, 8	ordtypelem3 9425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
68	66, 52, 67	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
69	65, 68	eqeltrd 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
70		breq2 5102	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = (𝑂‘𝑎) → (𝑢𝑅𝑣 ↔ 𝑢𝑅(𝑂‘𝑎)))
71	70	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑂‘𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂‘𝑎)))
72	71	ralbidv 3159	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑂‘𝑎) → (∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)))
73	72	elrab 3646	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂‘𝑎) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)))
74	73	simprbi 496	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))
75	69, 74	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))
76		breq2 5102	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑁 → (𝑗𝑅𝑤 ↔ 𝑗𝑅𝑁))
77	76	ralbidv 3159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁))
78		eldifi 4083	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁 ∈ 𝐴)
79	78	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ 𝐴)
80		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)
81	41	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂)
82	48, 81	fssdmd 6680	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹))
83	82, 12	sstrdi 3946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ 𝑇)
84		fveq1 6833	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑂 = (𝐹 ↾ 𝑇) → (𝑂‘𝑏) = ((𝐹 ↾ 𝑇)‘𝑏))
85		ssel2 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝑇)
86	85	fvresd 6854	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏))
87	84, 86	sylan9eq 2791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ (𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎)) → (𝑂‘𝑏) = (𝐹‘𝑏))
88	87	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → (𝑂‘𝑏) = (𝐹‘𝑏))
89	88	breq1d 5108	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → ((𝑂‘𝑏)𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁))
90	89	ralbidva 3157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
91	61, 83, 90	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
92	80, 91	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)
93	31	simpli 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Fun 𝐹
94		funfn 6522	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
95	93, 94	mpbi 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 Fn dom 𝐹
96		inss2 4190	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
97	82, 96	sstrdi 3946	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹)
98		breq1 5101	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝐹‘𝑏) → (𝑗𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁))
99	98	ralima 7183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
100	95, 97, 99	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
101	92, 100	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)
102	77, 79, 101	elrabd 3648	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤})
103	59, 75, 102	rspcdva 3577	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂‘𝑎))
104		weso 5615	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
105	7, 104	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 Or 𝐴)
106	105	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑅 Or 𝐴)
107	48, 52	ffvelcdmd 7030	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ 𝐴)
108		sotric 5562	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝐴 ∧ ((𝑂‘𝑎) ∈ 𝐴 ∧ 𝑁 ∈ 𝐴)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎))))
109	106, 107, 79, 108	syl12anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎))))
110		ioran 985	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)) ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎)))
111	109, 110	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎))))
112	57, 103, 111	mpbir2and 713	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎)𝑅𝑁)
113	112	expr 456	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 → (𝑂‘𝑎)𝑅𝑁))
114	45, 113	sylbid 240	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁))
115	114	ex 412	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁)))
116	115	com23 86	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))
117	116	a2i 14	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))
118	117	a1i 11	. . . . . . . . . 10 ⊢ (𝑎 ∈ On → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))))
119	30, 118	biimtrid 242	. . . . . . . . 9 ⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))))
120	24, 29, 119	tfis3 7800	. . . . . . . 8 ⊢ (𝑀 ∈ On → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))
121	120	com3l 89	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂‘𝑀)𝑅𝑁)))
122	19, 121	mpdd 43	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
123	1, 122	sylan2br 595	. . . . 5 ⊢ ((𝜑 ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
124	123	anassrs 467	. . . 4 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
125	124	impancom 451	. . 3 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂‘𝑀)𝑅𝑁))
126	125	orrd 863	. 2 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂‘𝑀)𝑅𝑁))
127	126	orcomd 871	1 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∃wrex 3060  {crab 3399  Vcvv 3440   ∖ cdif 3898   ∩ cin 3900   ⊆ wss 3901   class class class wbr 5098   ↦ cmpt 5179   Or wor 5531   Se wse 5575   We wwe 5576  dom cdm 5624  ran crn 5625   ↾ cres 5626   “ cima 5627  Ord word 6316  Oncon0 6317  Lim wlim 6318  Fun wfun 6486   Fn wfn 6487  ⟶wf 6488  ‘cfv 6492  ℩crio 7314  recscrecs 8302  OrdIsocoi 9414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rmo 3350  df-reu 3351  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-pss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-iun 4948  df-br 5099  df-opab 5161  df-mpt 5180  df-tr 5206  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-se 5578  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7315  df-ov 7361  df-2nd 7934  df-frecs 8223  df-wrecs 8254  df-recs 8303  df-oi 9415

This theorem is referenced by:  ordtypelem9  9431  ordtypelem10  9432  oiiniseg  9438