Step | Hyp | Ref
| Expression |
1 | | eldif 3550 |
. . . . . 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 8309 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
10 | 9 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
11 | | fdm 5964 |
. . . . . . . . . 10
⊢ (𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴 → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
13 | | inss1 3795 |
. . . . . . . . . 10
⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇 |
14 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem2 8307 |
. . . . . . . . . . . 12
⊢ (𝜑 → Ord 𝑇) |
15 | 14 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇) |
16 | | ordsson 6881 |
. . . . . . . . . . 11
⊢ (Ord
𝑇 → 𝑇 ⊆ On) |
17 | 15, 16 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On) |
18 | 13, 17 | syl5ss 3579 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On) |
19 | 12, 18 | eqsstrd 3602 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On) |
20 | 19 | sseld 3567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → 𝑀 ∈ On)) |
21 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂 ↔ 𝑏 ∈ dom 𝑂)) |
22 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑂‘𝑎) = (𝑂‘𝑏)) |
23 | 22 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑏)𝑅𝑁)) |
24 | 21, 23 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))) |
25 | 24 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))) |
26 | | eleq1 2676 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂 ↔ 𝑀 ∈ dom 𝑂)) |
27 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑀 → (𝑂‘𝑎) = (𝑂‘𝑀)) |
28 | 27 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑀 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑀)𝑅𝑁)) |
29 | 26, 28 | imbi12d 333 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))) |
30 | 29 | imbi2d 329 |
. . . . . . . . 9
⊢ (𝑎 = 𝑀 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))) |
31 | | r19.21v 2943 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))) |
32 | 2 | tfr1a 7377 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) |
33 | 32 | simpri 477 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Lim dom
𝐹 |
34 | | limord 5701 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim dom
𝐹 → Ord dom 𝐹) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ Ord dom
𝐹 |
36 | | ordin 5670 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord
𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹)) |
37 | 15, 35, 36 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹)) |
38 | | ordeq 5647 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹))) |
39 | 12, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹))) |
40 | 37, 39 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂) |
41 | | ordelss 5656 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Ord dom
𝑂 ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂) |
42 | 40, 41 | sylan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂) |
43 | 42 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ dom 𝑂) |
44 | | pm5.5 350 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁)) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁)) |
46 | 45 | ralbidva 2968 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) |
47 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂) |
48 | 47 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂) |
49 | 9 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) |
50 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴 → 𝑂 Fn (𝑇 ∩ dom 𝐹)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹)) |
52 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂) |
53 | 49, 11 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) |
54 | 52, 53 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹)) |
55 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂‘𝑎) ∈ ran 𝑂) |
56 | 51, 54, 55 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ ran 𝑂) |
57 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑎) = 𝑁 → ((𝑂‘𝑎) ∈ ran 𝑂 ↔ 𝑁 ∈ ran 𝑂)) |
58 | 56, 57 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎) = 𝑁 → 𝑁 ∈ ran 𝑂)) |
59 | 48, 58 | mtod 188 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ (𝑂‘𝑎) = 𝑁) |
60 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁 ∈ 𝐴) |
61 | 60 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ 𝐴) |
62 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁) |
63 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem1 8306 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) |
64 | 63 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 = (𝐹 ↾ 𝑇)) |
65 | 42 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂) |
66 | 65, 53 | sseqtrd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹)) |
67 | 66, 13 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ 𝑇) |
68 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑂 = (𝐹 ↾ 𝑇) → (𝑂‘𝑏) = ((𝐹 ↾ 𝑇)‘𝑏)) |
69 | | ssel2 3563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝑇) |
70 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏 ∈ 𝑇 → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏)) |
72 | 68, 71 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ (𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎)) → (𝑂‘𝑏) = (𝐹‘𝑏)) |
73 | 72 | anassrs 678 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → (𝑂‘𝑏) = (𝐹‘𝑏)) |
74 | 73 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → ((𝑂‘𝑏)𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁)) |
75 | 74 | ralbidva 2968 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
76 | 64, 67, 75 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
77 | 62, 76 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁) |
78 | 32 | simpli 473 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Fun 𝐹 |
79 | | funfn 5833 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
80 | 78, 79 | mpbi 219 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐹 Fn dom 𝐹 |
81 | | inss2 3796 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹 |
82 | 66, 81 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹) |
83 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝐹‘𝑏) → (𝑗𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁)) |
84 | 83 | ralima 6402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
85 | 80, 82, 84 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) |
86 | 77, 85 | mpbird 246 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁) |
87 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑁 → (𝑗𝑅𝑤 ↔ 𝑗𝑅𝑁)) |
88 | 87 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)) |
89 | 88 | elrab 3331 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ↔ (𝑁 ∈ 𝐴 ∧ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)) |
90 | 61, 86, 89 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤}) |
91 | 64 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = ((𝐹 ↾ 𝑇)‘𝑎)) |
92 | 13, 54 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ 𝑇) |
93 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 ∈ 𝑇 → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎)) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎)) |
95 | 91, 94 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = (𝐹‘𝑎)) |
96 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝜑) |
97 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem3 8308 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
98 | 96, 54, 97 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
99 | 95, 98 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) |
100 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = (𝑂‘𝑎) → (𝑢𝑅𝑣 ↔ 𝑢𝑅(𝑂‘𝑎))) |
101 | 100 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (𝑂‘𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂‘𝑎))) |
102 | 101 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝑂‘𝑎) → (∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))) |
103 | 102 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂‘𝑎) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))) |
104 | 103 | simprbi 479 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)) |
105 | 99, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)) |
106 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 = 𝑁 → (𝑢𝑅(𝑂‘𝑎) ↔ 𝑁𝑅(𝑂‘𝑎))) |
107 | 106 | notbid 307 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂‘𝑎) ↔ ¬ 𝑁𝑅(𝑂‘𝑎))) |
108 | 107 | rspcv 3278 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} → (∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎) → ¬ 𝑁𝑅(𝑂‘𝑎))) |
109 | 90, 105, 108 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂‘𝑎)) |
110 | | weso 5029 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
111 | 7, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 Or 𝐴) |
112 | 111 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑅 Or 𝐴) |
113 | 49, 54 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ 𝐴) |
114 | | sotric 4985 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 Or 𝐴 ∧ ((𝑂‘𝑎) ∈ 𝐴 ∧ 𝑁 ∈ 𝐴)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)))) |
115 | 112, 113,
61, 114 | syl12anc 1316 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)))) |
116 | | ioran 510 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)) ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎))) |
117 | 115, 116 | syl6bb 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎)))) |
118 | 59, 109, 117 | mpbir2and 959 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎)𝑅𝑁) |
119 | 118 | expr 641 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 → (𝑂‘𝑎)𝑅𝑁)) |
120 | 46, 119 | sylbid 229 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁)) |
121 | 120 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁))) |
122 | 121 | com23 84 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))) |
123 | 122 | a2i 14 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))) |
124 | 123 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑎 ∈ On → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))) |
125 | 31, 124 | syl5bi 231 |
. . . . . . . . 9
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))) |
126 | 25, 30, 125 | tfis3 6949 |
. . . . . . . 8
⊢ (𝑀 ∈ On → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))) |
127 | 126 | com3l 87 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂‘𝑀)𝑅𝑁))) |
128 | 20, 127 | mpdd 42 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
129 | 1, 128 | sylan2br 492 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
130 | 129 | anassrs 678 |
. . . 4
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
131 | 130 | impancom 455 |
. . 3
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂‘𝑀)𝑅𝑁)) |
132 | 131 | orrd 392 |
. 2
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂‘𝑀)𝑅𝑁)) |
133 | 132 | orcomd 402 |
1
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂)) |