Theorem ordtypelem7 9593

Description: Lemma for ordtype 9601. 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 3986	. . . . . 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 9590	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
10	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
11	10	fdmd 6757	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
12		inss1 4258	. . . . . . . . . 10 ⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇
13	2, 3, 4, 5, 6, 7, 8	ordtypelem2 9588	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝑇)
14	13	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇)
15		ordsson 7818	. . . . . . . . . . 11 ⊢ (Ord 𝑇 → 𝑇 ⊆ On)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On)
17	12, 16	sstrid 4020	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On)
18	11, 17	eqsstrd 4047	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On)
19	18	sseld 4007	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → 𝑀 ∈ On))
20		eleq1 2832	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂 ↔ 𝑏 ∈ dom 𝑂))
21		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (𝑂‘𝑎) = (𝑂‘𝑏))
22	21	breq1d 5176	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑏)𝑅𝑁))
23	20, 22	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))
24	23	imbi2d 340	. . . . . . . . 9 ⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))))
25		eleq1 2832	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂 ↔ 𝑀 ∈ dom 𝑂))
26		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑀 → (𝑂‘𝑎) = (𝑂‘𝑀))
27	26	breq1d 5176	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑀 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑀)𝑅𝑁))
28	25, 27	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))
29	28	imbi2d 340	. . . . . . . . 9 ⊢ (𝑎 = 𝑀 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))))
30		r19.21v 3186	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ 𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))
31	2	tfr1a 8450	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐹 ∧ Lim dom 𝐹)
32	31	simpri 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Lim dom 𝐹
33		limord 6455	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Lim dom 𝐹 → Ord dom 𝐹)
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐹
35		ordin 6425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹))
36	14, 34, 35	sylancl 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹))
37		ordeq 6402	. . . . . . . . . . . . . . . . . . . . 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 6411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord dom 𝑂 ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
41	39, 40	sylan 579	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
42	41	sselda 4008	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ dom 𝑂)
43		pm5.5 361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁))
44	42, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁))
45	44	ralbidva 3182	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁))
46		eldifn 4155	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂)
47	46	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂)
48	9	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
49	48	ffnd 6748	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹))
50		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂)
51	48	fdmd 6757	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
52	50, 51	eleqtrd 2846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹))
53		fnfvelrn 7114	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂‘𝑎) ∈ ran 𝑂)
54	49, 52, 53	syl2anc 583	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ ran 𝑂)
55		eleq1 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑂‘𝑎) = 𝑁 → ((𝑂‘𝑎) ∈ ran 𝑂 ↔ 𝑁 ∈ ran 𝑂))
56	54, 55	syl5ibcom 245	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎) = 𝑁 → 𝑁 ∈ ran 𝑂))
57	47, 56	mtod 198	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ (𝑂‘𝑎) = 𝑁)
58		breq1 5169	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑁 → (𝑢𝑅(𝑂‘𝑎) ↔ 𝑁𝑅(𝑂‘𝑎)))
59	58	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂‘𝑎) ↔ ¬ 𝑁𝑅(𝑂‘𝑎)))
60	2, 3, 4, 5, 6, 7, 8	ordtypelem1 9587	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇))
61	60	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 = (𝐹 ↾ 𝑇))
62	61	fveq1d 6922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = ((𝐹 ↾ 𝑇)‘𝑎))
63	52	elin1d 4227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ 𝑇)
64	63	fvresd 6940	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎))
65	62, 64	eqtrd 2780	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = (𝐹‘𝑎))
66		simpll 766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝜑)
67	2, 3, 4, 5, 6, 7, 8	ordtypelem3 9589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
68	66, 52, 67	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
69	65, 68	eqeltrd 2844	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
70		breq2 5170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = (𝑂‘𝑎) → (𝑢𝑅𝑣 ↔ 𝑢𝑅(𝑂‘𝑎)))
71	70	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑂‘𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂‘𝑎)))
72	71	ralbidv 3184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑂‘𝑎) → (∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)))
73	72	elrab 3708	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂‘𝑎) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)))
74	73	simprbi 496	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))
75	69, 74	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))
76		breq2 5170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑁 → (𝑗𝑅𝑤 ↔ 𝑗𝑅𝑁))
77	76	ralbidv 3184	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁))
78		eldifi 4154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁 ∈ 𝐴)
79	78	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ 𝐴)
80		simprr 772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)
81	41	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂)
82	48, 81	fssdmd 6765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹))
83	82, 12	sstrdi 4021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ 𝑇)
84		fveq1 6919	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑂 = (𝐹 ↾ 𝑇) → (𝑂‘𝑏) = ((𝐹 ↾ 𝑇)‘𝑏))
85		ssel2 4003	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝑇)
86	85	fvresd 6940	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏))
87	84, 86	sylan9eq 2800	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ (𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎)) → (𝑂‘𝑏) = (𝐹‘𝑏))
88	87	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → (𝑂‘𝑏) = (𝐹‘𝑏))
89	88	breq1d 5176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → ((𝑂‘𝑏)𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁))
90	89	ralbidva 3182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
91	61, 83, 90	syl2anc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
92	80, 91	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)
93	31	simpli 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Fun 𝐹
94		funfn 6608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
95	93, 94	mpbi 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 Fn dom 𝐹
96		inss2 4259	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
97	82, 96	sstrdi 4021	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹)
98		breq1 5169	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝐹‘𝑏) → (𝑗𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁))
99	98	ralima 7274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
100	95, 97, 99	sylancr 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
101	92, 100	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)
102	77, 79, 101	elrabd 3710	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤})
103	59, 75, 102	rspcdva 3636	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂‘𝑎))
104		weso 5691	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
105	7, 104	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 Or 𝐴)
106	105	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑅 Or 𝐴)
107	48, 52	ffvelcdmd 7119	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ 𝐴)
108		sotric 5637	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝐴 ∧ ((𝑂‘𝑎) ∈ 𝐴 ∧ 𝑁 ∈ 𝐴)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎))))
109	106, 107, 79, 108	syl12anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎))))
110		ioran 984	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)) ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎)))
111	109, 110	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎))))
112	57, 103, 111	mpbir2and 712	. . . . . . . . . . . . . . . 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 7895	. . . . . . . 8 ⊢ (𝑀 ∈ On → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))
121	120	com3l 89	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂‘𝑀)𝑅𝑁)))
122	19, 121	mpdd 43	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
123	1, 122	sylan2br 594	. . . . 5 ⊢ ((𝜑 ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
124	123	anassrs 467	. . . 4 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
125	124	impancom 451	. . 3 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂‘𝑀)𝑅𝑁))
126	125	orrd 862	. 2 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂‘𝑀)𝑅𝑁))
127	126	orcomd 870	1 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076  {crab 3443  Vcvv 3488   ∖ cdif 3973   ∩ cin 3975   ⊆ wss 3976   class class class wbr 5166   ↦ cmpt 5249   Or wor 5606   Se wse 5650   We wwe 5651  dom cdm 5700  ran crn 5701   ↾ cres 5702   “ cima 5703  Ord word 6394  Oncon0 6395  Lim wlim 6396  Fun wfun 6567   Fn wfn 6568  ⟶wf 6569  ‘cfv 6573  ℩crio 7403  recscrecs 8426  OrdIsocoi 9578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rmo 3388  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-se 5653  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-lim 6400  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-riota 7404  df-ov 7451  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427  df-oi 9579

This theorem is referenced by:  ordtypelem9  9595  ordtypelem10  9596  oiiniseg  9602