Theorem ordtypelem7 9439

Description: Lemma for ordtype 9447. 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 3899	. . . . . 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 9436	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
10	9	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
11	10	fdmd 6678	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
12		inss1 4177	. . . . . . . . . 10 ⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇
13	2, 3, 4, 5, 6, 7, 8	ordtypelem2 9434	. . . . . . . . . . . 12 ⊢ (𝜑 → Ord 𝑇)
14	13	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇)
15		ordsson 7737	. . . . . . . . . . 11 ⊢ (Ord 𝑇 → 𝑇 ⊆ On)
16	14, 15	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On)
17	12, 16	sstrid 3933	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On)
18	11, 17	eqsstrd 3956	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On)
19	18	sseld 3920	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → 𝑀 ∈ On))
20		eleq1 2824	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂 ↔ 𝑏 ∈ dom 𝑂))
21		fveq2 6840	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑏 → (𝑂‘𝑎) = (𝑂‘𝑏))
22	21	breq1d 5095	. . . . . . . . . . 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 6840	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑀 → (𝑂‘𝑎) = (𝑂‘𝑀))
27	26	breq1d 5095	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑀 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑀)𝑅𝑁))
28	25, 27	imbi12d 344	. . . . . . . . . 10 ⊢ (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))
29	28	imbi2d 340	. . . . . . . . 9 ⊢ (𝑎 = 𝑀 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))))
30		r19.21v 3162	. . . . . . . . . 10 ⊢ (∀𝑏 ∈ 𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))
31	2	tfr1a 8333	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐹 ∧ Lim dom 𝐹)
32	31	simpri 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Lim dom 𝐹
33		limord 6384	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Lim dom 𝐹 → Ord dom 𝐹)
34	32, 33	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ Ord dom 𝐹
35		ordin 6353	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((Ord 𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹))
36	14, 34, 35	sylancl 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹))
37		ordeq 6330	. . . . . . . . . . . . . . . . . . . . 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 6339	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Ord dom 𝑂 ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
41	39, 40	sylan 581	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
42	41	sselda 3921	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ dom 𝑂)
43		pm5.5 361	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁))
44	42, 43	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁))
45	44	ralbidva 3158	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁))
46		eldifn 4072	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂)
47	46	ad2antlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂)
48	9	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
49	48	ffnd 6669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹))
50		simprl 771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂)
51	48	fdmd 6678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
52	50, 51	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹))
53		fnfvelrn 7032	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂‘𝑎) ∈ ran 𝑂)
54	49, 52, 53	syl2anc 585	. . . . . . . . . . . . . . . . . . 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 5088	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑁 → (𝑢𝑅(𝑂‘𝑎) ↔ 𝑁𝑅(𝑂‘𝑎)))
59	58	notbid 318	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂‘𝑎) ↔ ¬ 𝑁𝑅(𝑂‘𝑎)))
60	2, 3, 4, 5, 6, 7, 8	ordtypelem1 9433	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇))
61	60	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 = (𝐹 ↾ 𝑇))
62	61	fveq1d 6842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = ((𝐹 ↾ 𝑇)‘𝑎))
63	52	elin1d 4144	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ 𝑇)
64	63	fvresd 6860	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎))
65	62, 64	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = (𝐹‘𝑎))
66		simpll 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝜑)
67	2, 3, 4, 5, 6, 7, 8	ordtypelem3 9435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
68	66, 52, 67	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
69	65, 68	eqeltrd 2836	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
70		breq2 5089	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = (𝑂‘𝑎) → (𝑢𝑅𝑣 ↔ 𝑢𝑅(𝑂‘𝑎)))
71	70	notbid 318	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑂‘𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂‘𝑎)))
72	71	ralbidv 3160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑂‘𝑎) → (∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)))
73	72	elrab 3634	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂‘𝑎) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)))
74	73	simprbi 497	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))
75	69, 74	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))
76		breq2 5089	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑁 → (𝑗𝑅𝑤 ↔ 𝑗𝑅𝑁))
77	76	ralbidv 3160	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁))
78		eldifi 4071	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁 ∈ 𝐴)
79	78	ad2antlr 728	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ 𝐴)
80		simprr 773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)
81	41	adantrr 718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂)
82	48, 81	fssdmd 6686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹))
83	82, 12	sstrdi 3934	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ 𝑇)
84		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑂 = (𝐹 ↾ 𝑇) → (𝑂‘𝑏) = ((𝐹 ↾ 𝑇)‘𝑏))
85		ssel2 3916	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝑇)
86	85	fvresd 6860	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏))
87	84, 86	sylan9eq 2791	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ (𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎)) → (𝑂‘𝑏) = (𝐹‘𝑏))
88	87	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → (𝑂‘𝑏) = (𝐹‘𝑏))
89	88	breq1d 5095	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → ((𝑂‘𝑏)𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁))
90	89	ralbidva 3158	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
91	61, 83, 90	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
92	80, 91	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)
93	31	simpli 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Fun 𝐹
94		funfn 6528	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (Fun 𝐹 ↔ 𝐹 Fn dom 𝐹)
95	93, 94	mpbi 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐹 Fn dom 𝐹
96		inss2 4178	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
97	82, 96	sstrdi 3934	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹)
98		breq1 5088	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 = (𝐹‘𝑏) → (𝑗𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁))
99	98	ralima 7192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
100	95, 97, 99	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁))
101	92, 100	mpbird 257	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)
102	77, 79, 101	elrabd 3636	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤})
103	59, 75, 102	rspcdva 3565	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂‘𝑎))
104		weso 5622	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴)
105	7, 104	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → 𝑅 Or 𝐴)
106	105	ad2antrr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑅 Or 𝐴)
107	48, 52	ffvelcdmd 7037	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ 𝐴)
108		sotric 5569	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 Or 𝐴 ∧ ((𝑂‘𝑎) ∈ 𝐴 ∧ 𝑁 ∈ 𝐴)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎))))
109	106, 107, 79, 108	syl12anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎))))
110		ioran 986	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)) ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎)))
111	109, 110	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎))))
112	57, 103, 111	mpbir2and 714	. . . . . . . . . . . . . . . 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 7809	. . . . . . . 8 ⊢ (𝑀 ∈ On → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))
121	120	com3l 89	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂‘𝑀)𝑅𝑁)))
122	19, 121	mpdd 43	. . . . . 6 ⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
123	1, 122	sylan2br 596	. . . . 5 ⊢ ((𝜑 ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
124	123	anassrs 467	. . . 4 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))
125	124	impancom 451	. . 3 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂‘𝑀)𝑅𝑁))
126	125	orrd 864	. 2 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂‘𝑀)𝑅𝑁))
127	126	orcomd 872	1 ⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061  {crab 3389  Vcvv 3429   ∖ cdif 3886   ∩ cin 3888   ⊆ wss 3889   class class class wbr 5085   ↦ cmpt 5166   Or wor 5538   Se wse 5582   We wwe 5583  dom cdm 5631  ran crn 5632   ↾ cres 5633   “ cima 5634  Ord word 6322  Oncon0 6323  Lim wlim 6324  Fun wfun 6492   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498  ℩crio 7323  recscrecs 8310  OrdIsocoi 9424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  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 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-oi 9425

This theorem is referenced by:  ordtypelem9  9441  ordtypelem10  9442  oiiniseg  9448