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

Theorem ordtypelem7 8782
Description: Lemma for ordtype 8790. 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 3834 . . . . . 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 8779 . . . . . . . . . . 11 (𝜑𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
109adantr 473 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
1110fdmd 6351 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
12 inss1 4087 . . . . . . . . . 10 (𝑇 ∩ dom 𝐹) ⊆ 𝑇
132, 3, 4, 5, 6, 7, 8ordtypelem2 8777 . . . . . . . . . . . 12 (𝜑 → Ord 𝑇)
1413adantr 473 . . . . . . . . . . 11 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇)
15 ordsson 7319 . . . . . . . . . . 11 (Ord 𝑇𝑇 ⊆ On)
1614, 15syl 17 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On)
1712, 16syl5ss 3864 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On)
1811, 17eqsstrd 3890 . . . . . . . 8 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On)
1918sseld 3852 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂𝑀 ∈ On))
20 eleq1 2848 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂𝑏 ∈ dom 𝑂))
21 fveq2 6497 . . . . . . . . . . . 12 (𝑎 = 𝑏 → (𝑂𝑎) = (𝑂𝑏))
2221breq1d 4936 . . . . . . . . . . 11 (𝑎 = 𝑏 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑏)𝑅𝑁))
2320, 22imbi12d 337 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
2423imbi2d 333 . . . . . . . . 9 (𝑎 = 𝑏 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁))))
25 eleq1 2848 . . . . . . . . . . 11 (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂𝑀 ∈ dom 𝑂))
26 fveq2 6497 . . . . . . . . . . . 12 (𝑎 = 𝑀 → (𝑂𝑎) = (𝑂𝑀))
2726breq1d 4936 . . . . . . . . . . 11 (𝑎 = 𝑀 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑀)𝑅𝑁))
2825, 27imbi12d 337 . . . . . . . . . 10 (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
2928imbi2d 333 . . . . . . . . 9 (𝑎 = 𝑀 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))))
30 r19.21v 3120 . . . . . . . . . 10 (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
312tfr1a 7833 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐹 ∧ Lim dom 𝐹)
3231simpri 478 . . . . . . . . . . . . . . . . . . . . . 22 Lim dom 𝐹
33 limord 6086 . . . . . . . . . . . . . . . . . . . . . 22 (Lim dom 𝐹 → Ord dom 𝐹)
3432, 33ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐹
35 ordin 6057 . . . . . . . . . . . . . . . . . . . . 21 ((Ord 𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹))
3614, 34, 35sylancl 578 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹))
37 ordeq 6034 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3811, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3936, 38mpbird 249 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂)
40 ordelss 6043 . . . . . . . . . . . . . . . . . . 19 ((Ord dom 𝑂𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4139, 40sylan 572 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4241sselda 3853 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → 𝑏 ∈ dom 𝑂)
43 pm5.5 354 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4442, 43syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4544ralbidva 3141 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁))
46 eldifn 3989 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂)
4746ad2antlr 715 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂)
489ad2antrr 714 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
4948ffnd 6343 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹))
50 simprl 759 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂)
5148fdmd 6351 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
5250, 51eleqtrd 2863 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹))
53 fnfvelrn 6672 . . . . . . . . . . . . . . . . . . . 20 ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂𝑎) ∈ ran 𝑂)
5449, 52, 53syl2anc 576 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ ran 𝑂)
55 eleq1 2848 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) = 𝑁 → ((𝑂𝑎) ∈ ran 𝑂𝑁 ∈ ran 𝑂))
5654, 55syl5ibcom 237 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎) = 𝑁𝑁 ∈ ran 𝑂))
5747, 56mtod 190 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ (𝑂𝑎) = 𝑁)
58 breq1 4929 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑁 → (𝑢𝑅(𝑂𝑎) ↔ 𝑁𝑅(𝑂𝑎)))
5958notbid 310 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂𝑎) ↔ ¬ 𝑁𝑅(𝑂𝑎)))
602, 3, 4, 5, 6, 7, 8ordtypelem1 8776 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑂 = (𝐹𝑇))
6160ad2antrr 714 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 = (𝐹𝑇))
6261fveq1d 6499 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = ((𝐹𝑇)‘𝑎))
6352elin1d 4058 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
6463fvresd 6517 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝐹𝑇)‘𝑎) = (𝐹𝑎))
6562, 64eqtrd 2809 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = (𝐹𝑎))
66 simpll 755 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝜑)
672, 3, 4, 5, 6, 7, 8ordtypelem3 8778 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
6866, 52, 67syl2anc 576 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
6965, 68eqeltrd 2861 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
70 breq2 4930 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (𝑂𝑎) → (𝑢𝑅𝑣𝑢𝑅(𝑂𝑎)))
7170notbid 310 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (𝑂𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂𝑎)))
7271ralbidv 3142 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝑂𝑎) → (∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7372elrab 3590 . . . . . . . . . . . . . . . . . . . 20 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂𝑎) ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7473simprbi 489 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
7569, 74syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
76 breq2 4930 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑁 → (𝑗𝑅𝑤𝑗𝑅𝑁))
7776ralbidv 3142 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁))
78 eldifi 3988 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁𝐴)
7978ad2antlr 715 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁𝐴)
80 simprr 761 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)
8141adantrr 705 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂)
8248, 81fssdmd 6357 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹))
8382, 12syl6ss 3865 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
84 fveq1 6496 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑂 = (𝐹𝑇) → (𝑂𝑏) = ((𝐹𝑇)‘𝑏))
85 ssel2 3848 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎𝑇𝑏𝑎) → 𝑏𝑇)
8685fvresd 6517 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝑇𝑏𝑎) → ((𝐹𝑇)‘𝑏) = (𝐹𝑏))
8784, 86sylan9eq 2829 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 = (𝐹𝑇) ∧ (𝑎𝑇𝑏𝑎)) → (𝑂𝑏) = (𝐹𝑏))
8887anassrs 460 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → (𝑂𝑏) = (𝐹𝑏))
8988breq1d 4936 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → ((𝑂𝑏)𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9089ralbidva 3141 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9161, 83, 90syl2anc 576 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9280, 91mpbid 224 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁)
9331simpli 476 . . . . . . . . . . . . . . . . . . . . . 22 Fun 𝐹
94 funfn 6216 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐹𝐹 Fn dom 𝐹)
9593, 94mpbi 222 . . . . . . . . . . . . . . . . . . . . 21 𝐹 Fn dom 𝐹
96 inss2 4088 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
9782, 96syl6ss 3865 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹)
98 breq1 4929 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝐹𝑏) → (𝑗𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9998ralima 6824 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Fn dom 𝐹𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10095, 97, 99sylancr 579 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10192, 100mpbird 249 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁)
10277, 79, 101elrabd 3593 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤})
10359, 75, 102rspcdva 3536 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂𝑎))
104 weso 5395 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 We 𝐴𝑅 Or 𝐴)
1057, 104syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 Or 𝐴)
106105ad2antrr 714 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑅 Or 𝐴)
10748, 52ffvelrnd 6676 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ 𝐴)
108 sotric 5350 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ ((𝑂𝑎) ∈ 𝐴𝑁𝐴)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
109106, 107, 79, 108syl12anc 825 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
110 ioran 967 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎)) ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎)))
111109, 110syl6bb 279 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎))))
11257, 103, 111mpbir2and 701 . . . . . . . . . . . . . . . 16 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎)𝑅𝑁)
113112expr 449 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 → (𝑂𝑎)𝑅𝑁))
11445, 113sylbid 232 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑂𝑎)𝑅𝑁))
115114ex 405 . . . . . . . . . . . . 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 234 . . . . . . . . 9 (𝑎 ∈ On → (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁))))
12024, 29, 119tfis3 7387 . . . . . . . 8 (𝑀 ∈ On → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
121120com3l 89 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂𝑀)𝑅𝑁)))
12219, 121mpdd 43 . . . . . 6 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
1231, 122sylan2br 586 . . . . 5 ((𝜑 ∧ (𝑁𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
124123anassrs 460 . . . 4 (((𝜑𝑁𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
125124impancom 444 . . 3 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂𝑀)𝑅𝑁))
126125orrd 850 . 2 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂𝑀)𝑅𝑁))
127126orcomd 858 1 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂𝑀)𝑅𝑁𝑁 ∈ ran 𝑂))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 834   = wceq 1508  wcel 2051  wral 3083  wrex 3084  {crab 3087  Vcvv 3410  cdif 3821  cin 3823  wss 3824   class class class wbr 4926  cmpt 5005   Or wor 5322   Se wse 5361   We wwe 5362  dom cdm 5404  ran crn 5405  cres 5406  cima 5407  Ord word 6026  Oncon0 6027  Lim wlim 6028  Fun wfun 6180   Fn wfn 6181  wf 6182  cfv 6186  crio 6935  recscrecs 7810  OrdIsocoi 8767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-pss 3840  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-tp 4441  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-tr 5028  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-wrecs 7749  df-recs 7811  df-oi 8768
This theorem is referenced by:  ordtypelem9  8784  ordtypelem10  8785  oiiniseg  8791
  Copyright terms: Public domain W3C validator