Step | Hyp | Ref
| Expression |
1 | | eldif 3725 |
. . . . . 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 8593 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
10 | 9 | adantr 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
11 | | fdm 6212 |
. . . . . . . . . 10
⊢ (𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴 → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
13 | | inss1 3976 |
. . . . . . . . . 10
⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇 |
14 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem2 8591 |
. . . . . . . . . . . 12
⊢ (𝜑 → Ord 𝑇) |
15 | 14 | adantr 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇) |
16 | | ordsson 7155 |
. . . . . . . . . . 11
⊢ (Ord
𝑇 → 𝑇 ⊆ On) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On) |
18 | 13, 17 | syl5ss 3755 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On) |
19 | 12, 18 | eqsstrd 3780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On) |
20 | 19 | sseld 3743 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → 𝑀 ∈ On)) |
21 | | eleq1 2827 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂 ↔ 𝑏 ∈ dom 𝑂)) |
22 | | fveq2 6353 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑂‘𝑎) = (𝑂‘𝑏)) |
23 | 22 | breq1d 4814 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑏)𝑅𝑁)) |
24 | 21, 23 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))) |
25 | 24 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))) |
26 | | eleq1 2827 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂 ↔ 𝑀 ∈ dom 𝑂)) |
27 | | fveq2 6353 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑀 → (𝑂‘𝑎) = (𝑂‘𝑀)) |
28 | 27 | breq1d 4814 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑀 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑀)𝑅𝑁)) |
29 | 26, 28 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))) |
30 | 29 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑎 = 𝑀 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))) |
31 | | r19.21v 3098 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))) |
32 | 2 | tfr1a 7660 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) |
33 | 32 | simpri 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Lim dom
𝐹 |
34 | | limord 5945 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim dom
𝐹 → Ord dom 𝐹) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ Ord dom
𝐹 |
36 | | ordin 5914 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord
𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹)) |
37 | 15, 35, 36 | sylancl 697 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹)) |
38 | | ordeq 5891 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹))) |
39 | 12, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹))) |
40 | 37, 39 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂) |
41 | | ordelss 5900 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Ord dom
𝑂 ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂) |
42 | 40, 41 | sylan 489 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂) |
43 | 42 | sselda 3744 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ dom 𝑂) |
44 | | pm5.5 350 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁)) |
46 | 45 | ralbidva 3123 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) |
47 | | eldifn 3876 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂) |
48 | 47 | ad2antlr 765 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂) |
49 | 9 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
50 | | ffn 6206 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴 → 𝑂 Fn (𝑇 ∩ dom 𝐹)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹)) |
52 | | simprl 811 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂) |
53 | 49, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
54 | 52, 53 | eleqtrd 2841 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹)) |
55 | | fnfvelrn 6520 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂‘𝑎) ∈ ran 𝑂) |
56 | 51, 54, 55 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ ran 𝑂) |
57 | | eleq1 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑎) = 𝑁 → ((𝑂‘𝑎) ∈ ran 𝑂 ↔ 𝑁 ∈ ran 𝑂)) |
58 | 56, 57 | syl5ibcom 235 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎) = 𝑁 → 𝑁 ∈ ran 𝑂)) |
59 | 48, 58 | mtod 189 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ (𝑂‘𝑎) = 𝑁) |
60 | | breq1 4807 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑁 → (𝑢𝑅(𝑂‘𝑎) ↔ 𝑁𝑅(𝑂‘𝑎))) |
61 | 60 | notbid 307 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂‘𝑎) ↔ ¬ 𝑁𝑅(𝑂‘𝑎))) |
62 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem1 8590 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) |
63 | 62 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 = (𝐹 ↾ 𝑇)) |
64 | 63 | fveq1d 6355 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = ((𝐹 ↾ 𝑇)‘𝑎)) |
65 | 13, 54 | sseldi 3742 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ 𝑇) |
66 | | fvres 6369 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ 𝑇 → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎)) |
68 | 64, 67 | eqtrd 2794 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = (𝐹‘𝑎)) |
69 | | simpll 807 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝜑) |
70 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem3 8592 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
71 | 69, 54, 70 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
72 | 68, 71 | eqeltrd 2839 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
73 | | breq2 4808 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = (𝑂‘𝑎) → (𝑢𝑅𝑣 ↔ 𝑢𝑅(𝑂‘𝑎))) |
74 | 73 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (𝑂‘𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂‘𝑎))) |
75 | 74 | ralbidv 3124 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝑂‘𝑎) → (∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))) |
76 | 75 | elrab 3504 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂‘𝑎) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))) |
77 | 76 | simprbi 483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)) |
78 | 72, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)) |
79 | | eldifi 3875 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁 ∈ 𝐴) |
80 | 79 | ad2antlr 765 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ 𝐴) |
81 | | simprr 813 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁) |
82 | 42 | adantrr 755 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂) |
83 | 82, 53 | sseqtrd 3782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹)) |
84 | 83, 13 | syl6ss 3756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ 𝑇) |
85 | | fveq1 6352 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑂 = (𝐹 ↾ 𝑇) → (𝑂‘𝑏) = ((𝐹 ↾ 𝑇)‘𝑏)) |
86 | | ssel2 3739 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝑇) |
87 | | fvres 6369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈ 𝑇 → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏)) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏)) |
89 | 85, 88 | sylan9eq 2814 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ (𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎)) → (𝑂‘𝑏) = (𝐹‘𝑏)) |
90 | 89 | anassrs 683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → (𝑂‘𝑏) = (𝐹‘𝑏)) |
91 | 90 | breq1d 4814 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → ((𝑂‘𝑏)𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁)) |
92 | 91 | ralbidva 3123 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
93 | 63, 84, 92 | syl2anc 696 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
94 | 81, 93 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁) |
95 | 32 | simpli 476 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Fun 𝐹 |
96 | | funfn 6079 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
97 | 95, 96 | mpbi 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐹 Fn dom 𝐹 |
98 | | inss2 3977 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹 |
99 | 83, 98 | syl6ss 3756 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹) |
100 | | breq1 4807 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝐹‘𝑏) → (𝑗𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁)) |
101 | 100 | ralima 6662 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
102 | 97, 99, 101 | sylancr 698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
103 | 94, 102 | mpbird 247 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁) |
104 | | breq2 4808 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑁 → (𝑗𝑅𝑤 ↔ 𝑗𝑅𝑁)) |
105 | 104 | ralbidv 3124 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)) |
106 | 105 | elrab 3504 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ↔ (𝑁 ∈ 𝐴 ∧ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)) |
107 | 80, 103, 106 | sylanbrc 701 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤}) |
108 | 61, 78, 107 | rspcdva 3455 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂‘𝑎)) |
109 | | weso 5257 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
110 | 7, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 Or 𝐴) |
111 | 110 | ad2antrr 764 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑅 Or 𝐴) |
112 | 49, 54 | ffvelrnd 6524 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ 𝐴) |
113 | | sotric 5213 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 Or 𝐴 ∧ ((𝑂‘𝑎) ∈ 𝐴 ∧ 𝑁 ∈ 𝐴)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)))) |
114 | 111, 112,
80, 113 | syl12anc 1475 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)))) |
115 | | ioran 512 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)) ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎))) |
116 | 114, 115 | syl6bb 276 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎)))) |
117 | 59, 108, 116 | mpbir2and 995 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎)𝑅𝑁) |
118 | 117 | expr 644 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 → (𝑂‘𝑎)𝑅𝑁)) |
119 | 46, 118 | sylbid 230 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁)) |
120 | 119 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁))) |
121 | 120 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))) |
122 | 121 | a2i 14 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))) |
123 | 122 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ On → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))) |
124 | 31, 123 | syl5bi 232 |
. . . . . . . . 9
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))) |
125 | 25, 30, 124 | tfis3 7223 |
. . . . . . . 8
⊢ (𝑀 ∈ On → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))) |
126 | 125 | com3l 89 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂‘𝑀)𝑅𝑁))) |
127 | 20, 126 | mpdd 43 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
128 | 1, 127 | sylan2br 494 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
129 | 128 | anassrs 683 |
. . . 4
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
130 | 129 | impancom 455 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
131 | 130 | orrd 392 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂‘𝑀)𝑅𝑁)) |
132 | 131 | orcomd 402 |
1
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂)) |