MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtypelem7 Structured version   Visualization version   GIF version

Theorem ordtypelem7 8976
Description: Lemma for ordtype 8984. 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.
StepHypRef Expression
1 eldif 3943 . . . . . 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 𝐴)
92, 3, 4, 5, 6, 7, 8ordtypelem4 8973 . . . . . . . . . . 11 (𝜑𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
109adantr 481 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
1110fdmd 6516 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
12 inss1 4202 . . . . . . . . . 10 (𝑇 ∩ dom 𝐹) ⊆ 𝑇
132, 3, 4, 5, 6, 7, 8ordtypelem2 8971 . . . . . . . . . . . 12 (𝜑 → Ord 𝑇)
1413adantr 481 . . . . . . . . . . 11 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇)
15 ordsson 7493 . . . . . . . . . . 11 (Ord 𝑇𝑇 ⊆ On)
1614, 15syl 17 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On)
1712, 16sstrid 3975 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On)
1811, 17eqsstrd 4002 . . . . . . . 8 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On)
1918sseld 3963 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂𝑀 ∈ On))
20 eleq1 2897 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂𝑏 ∈ dom 𝑂))
21 fveq2 6663 . . . . . . . . . . . 12 (𝑎 = 𝑏 → (𝑂𝑎) = (𝑂𝑏))
2221breq1d 5067 . . . . . . . . . . 11 (𝑎 = 𝑏 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑏)𝑅𝑁))
2320, 22imbi12d 346 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
2423imbi2d 342 . . . . . . . . 9 (𝑎 = 𝑏 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁))))
25 eleq1 2897 . . . . . . . . . . 11 (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂𝑀 ∈ dom 𝑂))
26 fveq2 6663 . . . . . . . . . . . 12 (𝑎 = 𝑀 → (𝑂𝑎) = (𝑂𝑀))
2726breq1d 5067 . . . . . . . . . . 11 (𝑎 = 𝑀 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑀)𝑅𝑁))
2825, 27imbi12d 346 . . . . . . . . . 10 (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
2928imbi2d 342 . . . . . . . . 9 (𝑎 = 𝑀 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))))
30 r19.21v 3172 . . . . . . . . . 10 (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
312tfr1a 8019 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐹 ∧ Lim dom 𝐹)
3231simpri 486 . . . . . . . . . . . . . . . . . . . . . 22 Lim dom 𝐹
33 limord 6243 . . . . . . . . . . . . . . . . . . . . . 22 (Lim dom 𝐹 → Ord dom 𝐹)
3432, 33ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐹
35 ordin 6214 . . . . . . . . . . . . . . . . . . . . 21 ((Ord 𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹))
3614, 34, 35sylancl 586 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹))
37 ordeq 6191 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3811, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3936, 38mpbird 258 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂)
40 ordelss 6200 . . . . . . . . . . . . . . . . . . 19 ((Ord dom 𝑂𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4139, 40sylan 580 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4241sselda 3964 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → 𝑏 ∈ dom 𝑂)
43 pm5.5 363 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4442, 43syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4544ralbidva 3193 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁))
46 eldifn 4101 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂)
4746ad2antlr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂)
489ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
4948ffnd 6508 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹))
50 simprl 767 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂)
5148fdmd 6516 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
5250, 51eleqtrd 2912 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹))
53 fnfvelrn 6840 . . . . . . . . . . . . . . . . . . . 20 ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂𝑎) ∈ ran 𝑂)
5449, 52, 53syl2anc 584 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ ran 𝑂)
55 eleq1 2897 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) = 𝑁 → ((𝑂𝑎) ∈ ran 𝑂𝑁 ∈ ran 𝑂))
5654, 55syl5ibcom 246 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎) = 𝑁𝑁 ∈ ran 𝑂))
5747, 56mtod 199 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ (𝑂𝑎) = 𝑁)
58 breq1 5060 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑁 → (𝑢𝑅(𝑂𝑎) ↔ 𝑁𝑅(𝑂𝑎)))
5958notbid 319 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂𝑎) ↔ ¬ 𝑁𝑅(𝑂𝑎)))
602, 3, 4, 5, 6, 7, 8ordtypelem1 8970 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑂 = (𝐹𝑇))
6160ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 = (𝐹𝑇))
6261fveq1d 6665 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = ((𝐹𝑇)‘𝑎))
6352elin1d 4172 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
6463fvresd 6683 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝐹𝑇)‘𝑎) = (𝐹𝑎))
6562, 64eqtrd 2853 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = (𝐹𝑎))
66 simpll 763 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝜑)
672, 3, 4, 5, 6, 7, 8ordtypelem3 8972 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
6866, 52, 67syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
6965, 68eqeltrd 2910 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
70 breq2 5061 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (𝑂𝑎) → (𝑢𝑅𝑣𝑢𝑅(𝑂𝑎)))
7170notbid 319 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (𝑂𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂𝑎)))
7271ralbidv 3194 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝑂𝑎) → (∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7372elrab 3677 . . . . . . . . . . . . . . . . . . . 20 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂𝑎) ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7473simprbi 497 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
7569, 74syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
76 breq2 5061 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑁 → (𝑗𝑅𝑤𝑗𝑅𝑁))
7776ralbidv 3194 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁))
78 eldifi 4100 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁𝐴)
7978ad2antlr 723 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁𝐴)
80 simprr 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)
8141adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂)
8248, 81fssdmd 6522 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹))
8382, 12sstrdi 3976 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
84 fveq1 6662 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑂 = (𝐹𝑇) → (𝑂𝑏) = ((𝐹𝑇)‘𝑏))
85 ssel2 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎𝑇𝑏𝑎) → 𝑏𝑇)
8685fvresd 6683 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝑇𝑏𝑎) → ((𝐹𝑇)‘𝑏) = (𝐹𝑏))
8784, 86sylan9eq 2873 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 = (𝐹𝑇) ∧ (𝑎𝑇𝑏𝑎)) → (𝑂𝑏) = (𝐹𝑏))
8887anassrs 468 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → (𝑂𝑏) = (𝐹𝑏))
8988breq1d 5067 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → ((𝑂𝑏)𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9089ralbidva 3193 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9161, 83, 90syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9280, 91mpbid 233 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁)
9331simpli 484 . . . . . . . . . . . . . . . . . . . . . 22 Fun 𝐹
94 funfn 6378 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐹𝐹 Fn dom 𝐹)
9593, 94mpbi 231 . . . . . . . . . . . . . . . . . . . . 21 𝐹 Fn dom 𝐹
96 inss2 4203 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
9782, 96sstrdi 3976 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹)
98 breq1 5060 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝐹𝑏) → (𝑗𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9998ralima 6991 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Fn dom 𝐹𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10095, 97, 99sylancr 587 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10192, 100mpbird 258 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁)
10277, 79, 101elrabd 3679 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤})
10359, 75, 102rspcdva 3622 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂𝑎))
104 weso 5539 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 We 𝐴𝑅 Or 𝐴)
1057, 104syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 Or 𝐴)
106105ad2antrr 722 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑅 Or 𝐴)
10748, 52ffvelrnd 6844 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ 𝐴)
108 sotric 5494 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ ((𝑂𝑎) ∈ 𝐴𝑁𝐴)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
109106, 107, 79, 108syl12anc 832 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
110 ioran 977 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎)) ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎)))
111109, 110syl6bb 288 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎))))
11257, 103, 111mpbir2and 709 . . . . . . . . . . . . . . . 16 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎)𝑅𝑁)
113112expr 457 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 → (𝑂𝑎)𝑅𝑁))
11445, 113sylbid 241 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑂𝑎)𝑅𝑁))
115114ex 413 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑂𝑎)𝑅𝑁)))
116115com23 86 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)))
117116a2i 14 . . . . . . . . . . 11 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)))
118117a1i 11 . . . . . . . . . 10 (𝑎 ∈ On → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁))))
11930, 118syl5bi 243 . . . . . . . . 9 (𝑎 ∈ On → (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁))))
12024, 29, 119tfis3 7561 . . . . . . . 8 (𝑀 ∈ On → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
121120com3l 89 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂𝑀)𝑅𝑁)))
12219, 121mpdd 43 . . . . . 6 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
1231, 122sylan2br 594 . . . . 5 ((𝜑 ∧ (𝑁𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
124123anassrs 468 . . . 4 (((𝜑𝑁𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
125124impancom 452 . . 3 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂𝑀)𝑅𝑁))
126125orrd 857 . 2 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂𝑀)𝑅𝑁))
127126orcomd 865 1 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂𝑀)𝑅𝑁𝑁 ∈ ran 𝑂))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  wral 3135  wrex 3136  {crab 3139  Vcvv 3492  cdif 3930  cin 3932  wss 3933   class class class wbr 5057  cmpt 5137   Or wor 5466   Se wse 5505   We wwe 5506  dom cdm 5548  ran crn 5549  cres 5550  cima 5551  Ord word 6183  Oncon0 6184  Lim wlim 6185  Fun wfun 6342   Fn wfn 6343  wf 6344  cfv 6348  crio 7102  recscrecs 7996  OrdIsocoi 8961
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-wrecs 7936  df-recs 7997  df-oi 8962
This theorem is referenced by:  ordtypelem9  8978  ordtypelem10  8979  oiiniseg  8985
  Copyright terms: Public domain W3C validator