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

Theorem ordtypelem7 8636
Description: Lemma for ordtype 8644. 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 3742 . . . . . 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 8633 . . . . . . . . . . 11 (𝜑𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
109adantr 472 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
1110fdmd 6232 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
12 inss1 3992 . . . . . . . . . 10 (𝑇 ∩ dom 𝐹) ⊆ 𝑇
132, 3, 4, 5, 6, 7, 8ordtypelem2 8631 . . . . . . . . . . . 12 (𝜑 → Ord 𝑇)
1413adantr 472 . . . . . . . . . . 11 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇)
15 ordsson 7187 . . . . . . . . . . 11 (Ord 𝑇𝑇 ⊆ On)
1614, 15syl 17 . . . . . . . . . 10 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On)
1712, 16syl5ss 3772 . . . . . . . . 9 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On)
1811, 17eqsstrd 3799 . . . . . . . 8 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On)
1918sseld 3760 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂𝑀 ∈ On))
20 eleq1 2832 . . . . . . . . . . 11 (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂𝑏 ∈ dom 𝑂))
21 fveq2 6375 . . . . . . . . . . . 12 (𝑎 = 𝑏 → (𝑂𝑎) = (𝑂𝑏))
2221breq1d 4819 . . . . . . . . . . 11 (𝑎 = 𝑏 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑏)𝑅𝑁))
2320, 22imbi12d 335 . . . . . . . . . 10 (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
2423imbi2d 331 . . . . . . . . 9 (𝑎 = 𝑏 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁))))
25 eleq1 2832 . . . . . . . . . . 11 (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂𝑀 ∈ dom 𝑂))
26 fveq2 6375 . . . . . . . . . . . 12 (𝑎 = 𝑀 → (𝑂𝑎) = (𝑂𝑀))
2726breq1d 4819 . . . . . . . . . . 11 (𝑎 = 𝑀 → ((𝑂𝑎)𝑅𝑁 ↔ (𝑂𝑀)𝑅𝑁))
2825, 27imbi12d 335 . . . . . . . . . 10 (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
2928imbi2d 331 . . . . . . . . 9 (𝑎 = 𝑀 → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))))
30 r19.21v 3107 . . . . . . . . . 10 (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) ↔ ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)))
312tfr1a 7694 . . . . . . . . . . . . . . . . . . . . . . 23 (Fun 𝐹 ∧ Lim dom 𝐹)
3231simpri 479 . . . . . . . . . . . . . . . . . . . . . 22 Lim dom 𝐹
33 limord 5967 . . . . . . . . . . . . . . . . . . . . . 22 (Lim dom 𝐹 → Ord dom 𝐹)
3432, 33ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21 Ord dom 𝐹
35 ordin 5938 . . . . . . . . . . . . . . . . . . . . 21 ((Ord 𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹))
3614, 34, 35sylancl 580 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹))
37 ordeq 5915 . . . . . . . . . . . . . . . . . . . . 21 (dom 𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3811, 37syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹)))
3936, 38mpbird 248 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂)
40 ordelss 5924 . . . . . . . . . . . . . . . . . . 19 ((Ord dom 𝑂𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4139, 40sylan 575 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂)
4241sselda 3761 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → 𝑏 ∈ dom 𝑂)
43 pm5.5 352 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4442, 43syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ (𝑂𝑏)𝑅𝑁))
4544ralbidva 3132 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) ↔ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁))
46 eldifn 3895 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂)
4746ad2antlr 718 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂)
489ad2antrr 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
4948ffnd 6224 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹))
50 simprl 787 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂)
5148fdmd 6232 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
5250, 51eleqtrd 2846 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹))
53 fnfvelrn 6546 . . . . . . . . . . . . . . . . . . . 20 ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂𝑎) ∈ ran 𝑂)
5449, 52, 53syl2anc 579 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ ran 𝑂)
55 eleq1 2832 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) = 𝑁 → ((𝑂𝑎) ∈ ran 𝑂𝑁 ∈ ran 𝑂))
5654, 55syl5ibcom 236 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎) = 𝑁𝑁 ∈ ran 𝑂))
5747, 56mtod 189 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ (𝑂𝑎) = 𝑁)
58 breq1 4812 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑁 → (𝑢𝑅(𝑂𝑎) ↔ 𝑁𝑅(𝑂𝑎)))
5958notbid 309 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂𝑎) ↔ ¬ 𝑁𝑅(𝑂𝑎)))
602, 3, 4, 5, 6, 7, 8ordtypelem1 8630 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑂 = (𝐹𝑇))
6160ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑂 = (𝐹𝑇))
6261fveq1d 6377 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = ((𝐹𝑇)‘𝑎))
6312, 52sseldi 3759 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
64 fvres 6394 . . . . . . . . . . . . . . . . . . . . . 22 (𝑎𝑇 → ((𝐹𝑇)‘𝑎) = (𝐹𝑎))
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝐹𝑇)‘𝑎) = (𝐹𝑎))
6662, 65eqtrd 2799 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) = (𝐹𝑎))
67 simpll 783 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝜑)
682, 3, 4, 5, 6, 7, 8ordtypelem3 8632 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
6967, 52, 68syl2anc 579 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝐹𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
7066, 69eqeltrd 2844 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
71 breq2 4813 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑣 = (𝑂𝑎) → (𝑢𝑅𝑣𝑢𝑅(𝑂𝑎)))
7271notbid 309 . . . . . . . . . . . . . . . . . . . . . 22 (𝑣 = (𝑂𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂𝑎)))
7372ralbidv 3133 . . . . . . . . . . . . . . . . . . . . 21 (𝑣 = (𝑂𝑎) → (∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7473elrab 3519 . . . . . . . . . . . . . . . . . . . 20 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂𝑎) ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎)))
7574simprbi 490 . . . . . . . . . . . . . . . . . . 19 ((𝑂𝑎) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
7670, 75syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂𝑎))
77 eldifi 3894 . . . . . . . . . . . . . . . . . . . 20 (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁𝐴)
7877ad2antlr 718 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁𝐴)
79 simprr 789 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)
8041adantrr 708 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂)
8148, 80fssdmd 6238 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹))
8281, 12syl6ss 3773 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎𝑇)
83 fveq1 6374 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑂 = (𝐹𝑇) → (𝑂𝑏) = ((𝐹𝑇)‘𝑏))
84 ssel2 3756 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑎𝑇𝑏𝑎) → 𝑏𝑇)
85 fvres 6394 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑏𝑇 → ((𝐹𝑇)‘𝑏) = (𝐹𝑏))
8684, 85syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑎𝑇𝑏𝑎) → ((𝐹𝑇)‘𝑏) = (𝐹𝑏))
8783, 86sylan9eq 2819 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑂 = (𝐹𝑇) ∧ (𝑎𝑇𝑏𝑎)) → (𝑂𝑏) = (𝐹𝑏))
8887anassrs 459 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → (𝑂𝑏) = (𝐹𝑏))
8988breq1d 4819 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) ∧ 𝑏𝑎) → ((𝑂𝑏)𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9089ralbidva 3132 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑂 = (𝐹𝑇) ∧ 𝑎𝑇) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9161, 82, 90syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
9279, 91mpbid 223 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁)
9331simpli 476 . . . . . . . . . . . . . . . . . . . . . 22 Fun 𝐹
94 funfn 6098 . . . . . . . . . . . . . . . . . . . . . 22 (Fun 𝐹𝐹 Fn dom 𝐹)
9593, 94mpbi 221 . . . . . . . . . . . . . . . . . . . . 21 𝐹 Fn dom 𝐹
96 inss2 3993 . . . . . . . . . . . . . . . . . . . . . 22 (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
9781, 96syl6ss 3773 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹)
98 breq1 4812 . . . . . . . . . . . . . . . . . . . . . 22 (𝑗 = (𝐹𝑏) → (𝑗𝑅𝑁 ↔ (𝐹𝑏)𝑅𝑁))
9998ralima 6691 . . . . . . . . . . . . . . . . . . . . 21 ((𝐹 Fn dom 𝐹𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10095, 97, 99sylancr 581 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁 ↔ ∀𝑏𝑎 (𝐹𝑏)𝑅𝑁))
10192, 100mpbird 248 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁)
102 breq2 4813 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 = 𝑁 → (𝑗𝑅𝑤𝑗𝑅𝑁))
103102ralbidv 3133 . . . . . . . . . . . . . . . . . . . 20 (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁))
104103elrab 3519 . . . . . . . . . . . . . . . . . . 19 (𝑁 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤} ↔ (𝑁𝐴 ∧ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑁))
10578, 101, 104sylanbrc 578 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑎)𝑗𝑅𝑤})
10659, 76, 105rspcdva 3467 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂𝑎))
107 weso 5268 . . . . . . . . . . . . . . . . . . . . 21 (𝑅 We 𝐴𝑅 Or 𝐴)
1087, 107syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝜑𝑅 Or 𝐴)
109108ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → 𝑅 Or 𝐴)
11048, 52ffvelrnd 6550 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎) ∈ 𝐴)
111 sotric 5224 . . . . . . . . . . . . . . . . . . 19 ((𝑅 Or 𝐴 ∧ ((𝑂𝑎) ∈ 𝐴𝑁𝐴)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
112109, 110, 78, 111syl12anc 865 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ ¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎))))
113 ioran 1006 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑂𝑎) = 𝑁𝑁𝑅(𝑂𝑎)) ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎)))
114112, 113syl6bb 278 . . . . . . . . . . . . . . . . 17 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → ((𝑂𝑎)𝑅𝑁 ↔ (¬ (𝑂𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂𝑎))))
11557, 106, 114mpbir2and 704 . . . . . . . . . . . . . . . 16 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏𝑎 (𝑂𝑏)𝑅𝑁)) → (𝑂𝑎)𝑅𝑁)
116115expr 448 . . . . . . . . . . . . . . 15 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑂𝑏)𝑅𝑁 → (𝑂𝑎)𝑅𝑁))
11745, 116sylbid 231 . . . . . . . . . . . . . 14 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑂𝑎)𝑅𝑁))
118117ex 401 . . . . . . . . . . . . 13 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑂𝑎)𝑅𝑁)))
119118com23 86 . . . . . . . . . . . 12 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)))
120119a2i 14 . . . . . . . . . . 11 (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁)))
121120a1i 11 . . . . . . . . . 10 (𝑎 ∈ On → (((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏𝑎 (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁))))
12230, 121syl5bi 233 . . . . . . . . 9 (𝑎 ∈ On → (∀𝑏𝑎 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂𝑏)𝑅𝑁)) → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂𝑎)𝑅𝑁))))
12324, 29, 122tfis3 7255 . . . . . . . 8 (𝑀 ∈ On → ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁)))
124123com3l 89 . . . . . . 7 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂𝑀)𝑅𝑁)))
12519, 124mpdd 43 . . . . . 6 ((𝜑𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
1261, 125sylan2br 588 . . . . 5 ((𝜑 ∧ (𝑁𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
127126anassrs 459 . . . 4 (((𝜑𝑁𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂𝑀)𝑅𝑁))
128127impancom 443 . . 3 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂𝑀)𝑅𝑁))
129128orrd 889 . 2 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂𝑀)𝑅𝑁))
130129orcomd 897 1 (((𝜑𝑁𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂𝑀)𝑅𝑁𝑁 ∈ ran 𝑂))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873   = wceq 1652  wcel 2155  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cdif 3729  cin 3731  wss 3732   class class class wbr 4809  cmpt 4888   Or wor 5197   Se wse 5234   We wwe 5235  dom cdm 5277  ran crn 5278  cres 5279  cima 5280  Ord word 5907  Oncon0 5908  Lim wlim 5909  Fun wfun 6062   Fn wfn 6063  wf 6064  cfv 6068  crio 6802  recscrecs 7671  OrdIsocoi 8621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-pss 3748  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-tp 4339  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-tr 4912  df-id 5185  df-eprel 5190  df-po 5198  df-so 5199  df-fr 5236  df-se 5237  df-we 5238  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-pred 5865  df-ord 5911  df-on 5912  df-lim 5913  df-suc 5914  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076  df-riota 6803  df-wrecs 7610  df-recs 7672  df-oi 8622
This theorem is referenced by:  ordtypelem9  8638  ordtypelem10  8639  oiiniseg  8645
  Copyright terms: Public domain W3C validator