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

Theorem ordtypelem7 9549
Description: Lemma for ordtype 9557. 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 3954 . . . . . 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 9546 . . . . . . . . . . 11 (𝜑𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
109adantr 479 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
1110fdmd 6733 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
12 inss1 4227 . . . . . . . . . 10 (𝑇 ∩ dom 𝐹) ⊆ 𝑇
132, 3, 4, 5, 6, 7, 8ordtypelem2 9544 . . . . . . . . . . . 12 (𝜑 → Ord 𝑇)
1413adantr 479 . . . . . . . . . . 11 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇)
15 ordsson 7786 . . . . . . . . . . 11 (Ord 𝑇𝑇 ⊆ On)
1614, 15syl 17 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On)
1712, 16sstrid 3988 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On)
1811, 17eqsstrd 4015 . . . . . . . 8 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On)
1918sseld 3975 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂𝑀 ∈ On))
20 eleq1 2813 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂𝑏 ∈ dom 𝑂))
21 fveq2 6896 . . . . . . . . . . . 12 (𝑎 = 𝑏 → (𝑂𝑎) = (𝑂𝑏))
2221breq1d 5159 . . . . . . . . . . 11 (𝑎 = 𝑏 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑏)𝑅𝑁))
2320, 22imbi12d 343 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
2423imbi2d 339 . . . . . . . . 9 (𝑎 = 𝑏 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁))))
25 eleq1 2813 . . . . . . . . . . 11 (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂𝑀 ∈ dom 𝑂))
26 fveq2 6896 . . . . . . . . . . . 12 (𝑎 = 𝑀 → (𝑂𝑎) = (𝑂𝑀))
2726breq1d 5159 . . . . . . . . . . 11 (𝑎 = 𝑀 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑀)𝑅𝑁))
2825, 27imbi12d 343 . . . . . . . . . 10 (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
2928imbi2d 339 . . . . . . . . 9 (𝑎 = 𝑀 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))))
30 r19.21v 3169 . . . . . . . . . 10 (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
312tfr1a 8415 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐹 ∧ Lim dom 𝐹)
3231simpri 484 . . . . . . . . . . . . . . . . . . . . . 22 Lim dom 𝐹
33 limord 6431 . . . . . . . . . . . . . . . . . . . . . 22 (Lim dom 𝐹 → Ord dom 𝐹)
3432, 33ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐹
35 ordin 6401 . . . . . . . . . . . . . . . . . . . . 21 ((Ord 𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹))
3614, 34, 35sylancl 584 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹))
37 ordeq 6378 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3811, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3936, 38mpbird 256 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂)
40 ordelss 6387 . . . . . . . . . . . . . . . . . . 19 ((Ord dom 𝑂𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4139, 40sylan 578 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4241sselda 3976 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → 𝑏 ∈ dom 𝑂)
43 pm5.5 360 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4442, 43syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4544ralbidva 3165 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁))
46 eldifn 4124 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂)
4746ad2antlr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂)
489ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
4948ffnd 6724 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹))
50 simprl 769 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂)
5148fdmd 6733 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
5250, 51eleqtrd 2827 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹))
53 fnfvelrn 7089 . . . . . . . . . . . . . . . . . . . 20 ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂𝑎) ∈ ran 𝑂)
5449, 52, 53syl2anc 582 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ ran 𝑂)
55 eleq1 2813 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) = 𝑁 → ((𝑂𝑎) ∈ ran 𝑂𝑁 ∈ ran 𝑂))
5654, 55syl5ibcom 244 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎) = 𝑁𝑁 ∈ ran 𝑂))
5747, 56mtod 197 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ (𝑂𝑎) = 𝑁)
58 breq1 5152 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑁 → (𝑢𝑅(𝑂𝑎) ↔ 𝑁𝑅(𝑂𝑎)))
5958notbid 317 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂𝑎) ↔ ¬ 𝑁𝑅(𝑂𝑎)))
602, 3, 4, 5, 6, 7, 8ordtypelem1 9543 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑂 = (𝐹𝑇))
6160ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 = (𝐹𝑇))
6261fveq1d 6898 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = ((𝐹𝑇)‘𝑎))
6352elin1d 4196 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
6463fvresd 6916 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝐹𝑇)‘𝑎) = (𝐹𝑎))
6562, 64eqtrd 2765 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = (𝐹𝑎))
66 simpll 765 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝜑)
672, 3, 4, 5, 6, 7, 8ordtypelem3 9545 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
6866, 52, 67syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
6965, 68eqeltrd 2825 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
70 breq2 5153 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (𝑂𝑎) → (𝑢𝑅𝑣𝑢𝑅(𝑂𝑎)))
7170notbid 317 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (𝑂𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂𝑎)))
7271ralbidv 3167 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝑂𝑎) → (∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7372elrab 3679 . . . . . . . . . . . . . . . . . . . 20 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂𝑎) ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7473simprbi 495 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
7569, 74syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
76 breq2 5153 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑁 → (𝑗𝑅𝑤𝑗𝑅𝑁))
7776ralbidv 3167 . . . . . . . . . . . . . . . . . . 19 (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁))
78 eldifi 4123 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁𝐴)
7978ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁𝐴)
80 simprr 771 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)
8141adantrr 715 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂)
8248, 81fssdmd 6741 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹))
8382, 12sstrdi 3989 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
84 fveq1 6895 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑂 = (𝐹𝑇) → (𝑂𝑏) = ((𝐹𝑇)‘𝑏))
85 ssel2 3971 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎𝑇𝑏𝑎) → 𝑏𝑇)
8685fvresd 6916 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝑇𝑏𝑎) → ((𝐹𝑇)‘𝑏) = (𝐹𝑏))
8784, 86sylan9eq 2785 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 = (𝐹𝑇) ∧ (𝑎𝑇𝑏𝑎)) → (𝑂𝑏) = (𝐹𝑏))
8887anassrs 466 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → (𝑂𝑏) = (𝐹𝑏))
8988breq1d 5159 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → ((𝑂𝑏)𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9089ralbidva 3165 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9161, 83, 90syl2anc 582 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9280, 91mpbid 231 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁)
9331simpli 482 . . . . . . . . . . . . . . . . . . . . . 22 Fun 𝐹
94 funfn 6584 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐹𝐹 Fn dom 𝐹)
9593, 94mpbi 229 . . . . . . . . . . . . . . . . . . . . 21 𝐹 Fn dom 𝐹
96 inss2 4228 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
9782, 96sstrdi 3989 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹)
98 breq1 5152 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝐹𝑏) → (𝑗𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9998ralima 7250 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Fn dom 𝐹𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10095, 97, 99sylancr 585 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10192, 100mpbird 256 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁)
10277, 79, 101elrabd 3681 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤})
10359, 75, 102rspcdva 3607 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂𝑎))
104 weso 5669 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 We 𝐴𝑅 Or 𝐴)
1057, 104syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 Or 𝐴)
106105ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑅 Or 𝐴)
10748, 52ffvelcdmd 7094 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ 𝐴)
108 sotric 5618 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ ((𝑂𝑎) ∈ 𝐴𝑁𝐴)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
109106, 107, 79, 108syl12anc 835 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
110 ioran 981 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎)) ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎)))
111109, 110bitrdi 286 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎))))
11257, 103, 111mpbir2and 711 . . . . . . . . . . . . . . . 16 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎)𝑅𝑁)
113112expr 455 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 → (𝑂𝑎)𝑅𝑁))
11445, 113sylbid 239 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑂𝑎)𝑅𝑁))
115114ex 411 . . . . . . . . . . . . 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, 118biimtrid 241 . . . . . . . . 9 (𝑎 ∈ On → (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁))))
12024, 29, 119tfis3 7863 . . . . . . . 8 (𝑀 ∈ On → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
121120com3l 89 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂𝑀)𝑅𝑁)))
12219, 121mpdd 43 . . . . . 6 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
1231, 122sylan2br 593 . . . . 5 ((𝜑 ∧ (𝑁𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
124123anassrs 466 . . . 4 (((𝜑𝑁𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
125124impancom 450 . . 3 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂𝑀)𝑅𝑁))
126125orrd 861 . 2 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂𝑀)𝑅𝑁))
127126orcomd 869 1 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂𝑀)𝑅𝑁𝑁 ∈ ran 𝑂))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 845   = wceq 1533  wcel 2098  wral 3050  wrex 3059  {crab 3418  Vcvv 3461  cdif 3941  cin 3943  wss 3944   class class class wbr 5149  cmpt 5232   Or wor 5589   Se wse 5631   We wwe 5632  dom cdm 5678  ran crn 5679  cres 5680  cima 5681  Ord word 6370  Oncon0 6371  Lim wlim 6372  Fun wfun 6543   Fn wfn 6544  wf 6545  cfv 6549  crio 7374  recscrecs 8391  OrdIsocoi 9534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-riota 7375  df-ov 7422  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-oi 9535
This theorem is referenced by:  ordtypelem9  9551  ordtypelem10  9552  oiiniseg  9558
  Copyright terms: Public domain W3C validator