| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eldif 3961 | . . . . . 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 9561 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) | 
| 10 | 9 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) | 
| 11 | 10 | fdmd 6746 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) | 
| 12 |  | inss1 4237 | . . . . . . . . . 10
⊢ (𝑇 ∩ dom 𝐹) ⊆ 𝑇 | 
| 13 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem2 9559 | . . . . . . . . . . . 12
⊢ (𝜑 → Ord 𝑇) | 
| 14 | 13 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord 𝑇) | 
| 15 |  | ordsson 7803 | . . . . . . . . . . 11
⊢ (Ord
𝑇 → 𝑇 ⊆ On) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → 𝑇 ⊆ On) | 
| 17 | 12, 16 | sstrid 3995 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑇 ∩ dom 𝐹) ⊆ On) | 
| 18 | 11, 17 | eqsstrd 4018 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → dom 𝑂 ⊆ On) | 
| 19 | 18 | sseld 3982 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → 𝑀 ∈ On)) | 
| 20 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → (𝑎 ∈ dom 𝑂 ↔ 𝑏 ∈ dom 𝑂)) | 
| 21 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑏 → (𝑂‘𝑎) = (𝑂‘𝑏)) | 
| 22 | 21 | breq1d 5153 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑏 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑏)𝑅𝑁)) | 
| 23 | 20, 22 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑎 = 𝑏 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))) | 
| 24 | 23 | imbi2d 340 | . . . . . . . . 9
⊢ (𝑎 = 𝑏 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)))) | 
| 25 |  | eleq1 2829 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑀 → (𝑎 ∈ dom 𝑂 ↔ 𝑀 ∈ dom 𝑂)) | 
| 26 |  | fveq2 6906 | . . . . . . . . . . . 12
⊢ (𝑎 = 𝑀 → (𝑂‘𝑎) = (𝑂‘𝑀)) | 
| 27 | 26 | breq1d 5153 | . . . . . . . . . . 11
⊢ (𝑎 = 𝑀 → ((𝑂‘𝑎)𝑅𝑁 ↔ (𝑂‘𝑀)𝑅𝑁)) | 
| 28 | 25, 27 | imbi12d 344 | . . . . . . . . . 10
⊢ (𝑎 = 𝑀 → ((𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁) ↔ (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))) | 
| 29 | 28 | imbi2d 340 | . . . . . . . . 9
⊢ (𝑎 = 𝑀 → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)))) | 
| 30 |  | r19.21v 3180 | . . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) ↔ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁))) | 
| 31 | 2 | tfr1a 8434 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Fun
𝐹 ∧ Lim dom 𝐹) | 
| 32 | 31 | simpri 485 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ Lim dom
𝐹 | 
| 33 |  | limord 6444 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim dom
𝐹 → Ord dom 𝐹) | 
| 34 | 32, 33 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . 21
⊢ Ord dom
𝐹 | 
| 35 |  | ordin 6414 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((Ord
𝑇 ∧ Ord dom 𝐹) → Ord (𝑇 ∩ dom 𝐹)) | 
| 36 | 14, 34, 35 | sylancl 586 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord (𝑇 ∩ dom 𝐹)) | 
| 37 |  | ordeq 6391 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (dom
𝑂 = (𝑇 ∩ dom 𝐹) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹))) | 
| 38 | 11, 37 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (Ord dom 𝑂 ↔ Ord (𝑇 ∩ dom 𝐹))) | 
| 39 | 36, 38 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → Ord dom 𝑂) | 
| 40 |  | ordelss 6400 | . . . . . . . . . . . . . . . . . . 19
⊢ ((Ord dom
𝑂 ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂) | 
| 41 | 39, 40 | sylan 580 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → 𝑎 ⊆ dom 𝑂) | 
| 42 | 41 | sselda 3983 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ dom 𝑂) | 
| 43 |  | pm5.5 361 | . . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ dom 𝑂 → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁)) | 
| 44 | 42, 43 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) ∧ 𝑏 ∈ 𝑎) → ((𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ (𝑂‘𝑏)𝑅𝑁)) | 
| 45 | 44 | ralbidva 3176 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) ↔ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) | 
| 46 |  | eldifn 4132 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → ¬ 𝑁 ∈ ran 𝑂) | 
| 47 | 46 | ad2antlr 727 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁 ∈ ran 𝑂) | 
| 48 | 9 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴) | 
| 49 | 48 | ffnd 6737 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 Fn (𝑇 ∩ dom 𝐹)) | 
| 50 |  | simprl 771 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ dom 𝑂) | 
| 51 | 48 | fdmd 6746 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → dom 𝑂 = (𝑇 ∩ dom 𝐹)) | 
| 52 | 50, 51 | eleqtrd 2843 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ (𝑇 ∩ dom 𝐹)) | 
| 53 |  | fnfvelrn 7100 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑂 Fn (𝑇 ∩ dom 𝐹) ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝑂‘𝑎) ∈ ran 𝑂) | 
| 54 | 49, 52, 53 | syl2anc 584 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ ran 𝑂) | 
| 55 |  | eleq1 2829 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑎) = 𝑁 → ((𝑂‘𝑎) ∈ ran 𝑂 ↔ 𝑁 ∈ ran 𝑂)) | 
| 56 | 54, 55 | syl5ibcom 245 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎) = 𝑁 → 𝑁 ∈ ran 𝑂)) | 
| 57 | 47, 56 | mtod 198 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ (𝑂‘𝑎) = 𝑁) | 
| 58 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑢 = 𝑁 → (𝑢𝑅(𝑂‘𝑎) ↔ 𝑁𝑅(𝑂‘𝑎))) | 
| 59 | 58 | notbid 318 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑁 → (¬ 𝑢𝑅(𝑂‘𝑎) ↔ ¬ 𝑁𝑅(𝑂‘𝑎))) | 
| 60 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem1 9558 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑂 = (𝐹 ↾ 𝑇)) | 
| 61 | 60 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑂 = (𝐹 ↾ 𝑇)) | 
| 62 | 61 | fveq1d 6908 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = ((𝐹 ↾ 𝑇)‘𝑎)) | 
| 63 | 52 | elin1d 4204 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ∈ 𝑇) | 
| 64 | 63 | fvresd 6926 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝐹 ↾ 𝑇)‘𝑎) = (𝐹‘𝑎)) | 
| 65 | 62, 64 | eqtrd 2777 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) = (𝐹‘𝑎)) | 
| 66 |  | simpll 767 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝜑) | 
| 67 | 2, 3, 4, 5, 6, 7, 8 | ordtypelem3 9560 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | 
| 68 | 66, 52, 67 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝐹‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | 
| 69 | 65, 68 | eqeltrd 2841 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣}) | 
| 70 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = (𝑂‘𝑎) → (𝑢𝑅𝑣 ↔ 𝑢𝑅(𝑂‘𝑎))) | 
| 71 | 70 | notbid 318 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 = (𝑂‘𝑎) → (¬ 𝑢𝑅𝑣 ↔ ¬ 𝑢𝑅(𝑂‘𝑎))) | 
| 72 | 71 | ralbidv 3178 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 = (𝑂‘𝑎) → (∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))) | 
| 73 | 72 | elrab 3692 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ↔ ((𝑂‘𝑎) ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∧ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎))) | 
| 74 | 73 | simprbi 496 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑂‘𝑎) ∈ {𝑣 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)) | 
| 75 | 69, 74 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑢 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤} ¬ 𝑢𝑅(𝑂‘𝑎)) | 
| 76 |  | breq2 5147 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑁 → (𝑗𝑅𝑤 ↔ 𝑗𝑅𝑁)) | 
| 77 | 76 | ralbidv 3178 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑁 → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁)) | 
| 78 |  | eldifi 4131 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ (𝐴 ∖ ran 𝑂) → 𝑁 ∈ 𝐴) | 
| 79 | 78 | ad2antlr 727 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ 𝐴) | 
| 80 |  | simprr 773 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁) | 
| 81 | 41 | adantrr 717 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝑂) | 
| 82 | 48, 81 | fssdmd 6754 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ (𝑇 ∩ dom 𝐹)) | 
| 83 | 82, 12 | sstrdi 3996 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ 𝑇) | 
| 84 |  | fveq1 6905 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑂 = (𝐹 ↾ 𝑇) → (𝑂‘𝑏) = ((𝐹 ↾ 𝑇)‘𝑏)) | 
| 85 |  | ssel2 3978 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → 𝑏 ∈ 𝑇) | 
| 86 | 85 | fvresd 6926 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎) → ((𝐹 ↾ 𝑇)‘𝑏) = (𝐹‘𝑏)) | 
| 87 | 84, 86 | sylan9eq 2797 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ (𝑎 ⊆ 𝑇 ∧ 𝑏 ∈ 𝑎)) → (𝑂‘𝑏) = (𝐹‘𝑏)) | 
| 88 | 87 | anassrs 467 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → (𝑂‘𝑏) = (𝐹‘𝑏)) | 
| 89 | 88 | breq1d 5153 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) ∧ 𝑏 ∈ 𝑎) → ((𝑂‘𝑏)𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁)) | 
| 90 | 89 | ralbidva 3176 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑂 = (𝐹 ↾ 𝑇) ∧ 𝑎 ⊆ 𝑇) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) | 
| 91 | 61, 83, 90 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) | 
| 92 | 80, 91 | mpbid 232 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁) | 
| 93 | 31 | simpli 483 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ Fun 𝐹 | 
| 94 |  | funfn 6596 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) | 
| 95 | 93, 94 | mpbi 230 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝐹 Fn dom 𝐹 | 
| 96 |  | inss2 4238 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹 | 
| 97 | 82, 96 | sstrdi 3996 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑎 ⊆ dom 𝐹) | 
| 98 |  | breq1 5146 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑗 = (𝐹‘𝑏) → (𝑗𝑅𝑁 ↔ (𝐹‘𝑏)𝑅𝑁)) | 
| 99 | 98 | ralima 7257 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐹 Fn dom 𝐹 ∧ 𝑎 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) | 
| 100 | 95, 97, 99 | sylancr 587 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁 ↔ ∀𝑏 ∈ 𝑎 (𝐹‘𝑏)𝑅𝑁)) | 
| 101 | 92, 100 | mpbird 257 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑁) | 
| 102 | 77, 79, 101 | elrabd 3694 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑁 ∈ {𝑤 ∈ 𝐴 ∣ ∀𝑗 ∈ (𝐹 “ 𝑎)𝑗𝑅𝑤}) | 
| 103 | 59, 75, 102 | rspcdva 3623 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ¬ 𝑁𝑅(𝑂‘𝑎)) | 
| 104 |  | weso 5676 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) | 
| 105 | 7, 104 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑅 Or 𝐴) | 
| 106 | 105 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → 𝑅 Or 𝐴) | 
| 107 | 48, 52 | ffvelcdmd 7105 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎) ∈ 𝐴) | 
| 108 |  | sotric 5622 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 Or 𝐴 ∧ ((𝑂‘𝑎) ∈ 𝐴 ∧ 𝑁 ∈ 𝐴)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)))) | 
| 109 | 106, 107,
79, 108 | syl12anc 837 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ ¬ ((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)))) | 
| 110 |  | ioran 986 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
((𝑂‘𝑎) = 𝑁 ∨ 𝑁𝑅(𝑂‘𝑎)) ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎))) | 
| 111 | 109, 110 | bitrdi 287 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → ((𝑂‘𝑎)𝑅𝑁 ↔ (¬ (𝑂‘𝑎) = 𝑁 ∧ ¬ 𝑁𝑅(𝑂‘𝑎)))) | 
| 112 | 57, 103, 111 | mpbir2and 713 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ (𝑎 ∈ dom 𝑂 ∧ ∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁)) → (𝑂‘𝑎)𝑅𝑁) | 
| 113 | 112 | expr 456 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑂‘𝑏)𝑅𝑁 → (𝑂‘𝑎)𝑅𝑁)) | 
| 114 | 45, 113 | sylbid 240 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) ∧ 𝑎 ∈ dom 𝑂) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁)) | 
| 115 | 114 | ex 412 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑂‘𝑎)𝑅𝑁))) | 
| 116 | 115 | com23 86 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))) | 
| 117 | 116 | a2i 14 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁))) | 
| 118 | 117 | a1i 11 | . . . . . . . . . 10
⊢ (𝑎 ∈ On → (((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → ∀𝑏 ∈ 𝑎 (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))) | 
| 119 | 30, 118 | biimtrid 242 | . . . . . . . . 9
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑏 ∈ dom 𝑂 → (𝑂‘𝑏)𝑅𝑁)) → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑎 ∈ dom 𝑂 → (𝑂‘𝑎)𝑅𝑁)))) | 
| 120 | 24, 29, 119 | tfis3 7879 | . . . . . . . 8
⊢ (𝑀 ∈ On → ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁))) | 
| 121 | 120 | com3l 89 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑀 ∈ On → (𝑂‘𝑀)𝑅𝑁))) | 
| 122 | 19, 121 | mpdd 43 | . . . . . 6
⊢ ((𝜑 ∧ 𝑁 ∈ (𝐴 ∖ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) | 
| 123 | 1, 122 | sylan2br 595 | . . . . 5
⊢ ((𝜑 ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ∈ ran 𝑂)) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) | 
| 124 | 123 | anassrs 467 | . . . 4
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ ¬ 𝑁 ∈ ran 𝑂) → (𝑀 ∈ dom 𝑂 → (𝑂‘𝑀)𝑅𝑁)) | 
| 125 | 124 | impancom 451 | . . 3
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (¬ 𝑁 ∈ ran 𝑂 → (𝑂‘𝑀)𝑅𝑁)) | 
| 126 | 125 | orrd 864 | . 2
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → (𝑁 ∈ ran 𝑂 ∨ (𝑂‘𝑀)𝑅𝑁)) | 
| 127 | 126 | orcomd 872 | 1
⊢ (((𝜑 ∧ 𝑁 ∈ 𝐴) ∧ 𝑀 ∈ dom 𝑂) → ((𝑂‘𝑀)𝑅𝑁 ∨ 𝑁 ∈ ran 𝑂)) |