| Step | Hyp | Ref
| Expression |
| 1 | | frss 5649 |
. . . 4
⊢ (𝐵 ⊆ 𝐴 → (𝑅 Fr 𝐴 → 𝑅 Fr 𝐵)) |
| 2 | | sess2 5651 |
. . . 4
⊢ (𝐵 ⊆ 𝐴 → (𝑅 Se 𝐴 → 𝑅 Se 𝐵)) |
| 3 | 1, 2 | anim12d 609 |
. . 3
⊢ (𝐵 ⊆ 𝐴 → ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → (𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵))) |
| 4 | | n0 4353 |
. . . 4
⊢ (𝐵 ≠ ∅ ↔
∃𝑏 𝑏 ∈ 𝐵) |
| 5 | | predeq3 6325 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐵, 𝑏)) |
| 6 | 5 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, 𝐵, 𝑏) = ∅)) |
| 7 | 6 | rspcev 3622 |
. . . . . . . . 9
⊢ ((𝑏 ∈ 𝐵 ∧ Pred(𝑅, 𝐵, 𝑏) = ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) |
| 8 | 7 | ex 412 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 9 | 8 | adantl 481 |
. . . . . . 7
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 10 | | predres 6360 |
. . . . . . . . . . 11
⊢
Pred(𝑅, 𝐵, 𝑏) = Pred((𝑅 ↾ 𝐵), 𝐵, 𝑏) |
| 11 | | relres 6023 |
. . . . . . . . . . . . 13
⊢ Rel
(𝑅 ↾ 𝐵) |
| 12 | | ssttrcl 9755 |
. . . . . . . . . . . . 13
⊢ (Rel
(𝑅 ↾ 𝐵) → (𝑅 ↾ 𝐵) ⊆ t++(𝑅 ↾ 𝐵)) |
| 13 | 11, 12 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (𝑅 ↾ 𝐵) ⊆ t++(𝑅 ↾ 𝐵) |
| 14 | | predrelss 6358 |
. . . . . . . . . . . 12
⊢ ((𝑅 ↾ 𝐵) ⊆ t++(𝑅 ↾ 𝐵) → Pred((𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)) |
| 15 | 13, 14 | ax-mp 5 |
. . . . . . . . . . 11
⊢
Pred((𝑅 ↾
𝐵), 𝐵, 𝑏) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) |
| 16 | 10, 15 | eqsstri 4030 |
. . . . . . . . . 10
⊢
Pred(𝑅, 𝐵, 𝑏) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) |
| 17 | | ssn0 4404 |
. . . . . . . . . 10
⊢
((Pred(𝑅, 𝐵, 𝑏) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∧ Pred(𝑅, 𝐵, 𝑏) ≠ ∅) → Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) |
| 18 | 16, 17 | mpan 690 |
. . . . . . . . 9
⊢
(Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) |
| 19 | | predss 6329 |
. . . . . . . . 9
⊢
Pred(t++(𝑅 ↾
𝐵), 𝐵, 𝑏) ⊆ 𝐵 |
| 20 | 18, 19 | jctil 519 |
. . . . . . . 8
⊢
(Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅)) |
| 21 | | dffr4 6341 |
. . . . . . . . . . . 12
⊢ (𝑅 Fr 𝐵 ↔ ∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) |
| 22 | 21 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝑅 Fr 𝐵 → ∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) |
| 23 | | ttrclse 9767 |
. . . . . . . . . . . . 13
⊢ (𝑅 Se 𝐵 → t++(𝑅 ↾ 𝐵) Se 𝐵) |
| 24 | | setlikespec 6346 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝐵 ∧ t++(𝑅 ↾ 𝐵) Se 𝐵) → Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∈ V) |
| 25 | 23, 24 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∈ V) |
| 26 | 25 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((𝑅 Se 𝐵 ∧ 𝑏 ∈ 𝐵) → Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∈ V) |
| 27 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) → (𝑐 ⊆ 𝐵 ↔ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵)) |
| 28 | | neeq1 3003 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) → (𝑐 ≠ ∅ ↔ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅)) |
| 29 | 27, 28 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) ↔ (Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅))) |
| 30 | | predeq2 6324 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) → Pred(𝑅, 𝑐, 𝑦) = Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦)) |
| 31 | 30 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) → (Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅)) |
| 32 | 31 | rexeqbi1dv 3339 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) → (∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ ∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅)) |
| 33 | 29, 32 | imbi12d 344 |
. . . . . . . . . . . . 13
⊢ (𝑐 = Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) → (((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) ↔ ((Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅))) |
| 34 | 33 | spcgv 3596 |
. . . . . . . . . . . 12
⊢
(Pred(t++(𝑅 ↾
𝐵), 𝐵, 𝑏) ∈ V → (∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) → ((Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅))) |
| 35 | 34 | impcom 407 |
. . . . . . . . . . 11
⊢
((∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∈ V) → ((Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅)) |
| 36 | 22, 26, 35 | syl2an 596 |
. . . . . . . . . 10
⊢ ((𝑅 Fr 𝐵 ∧ (𝑅 Se 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅)) |
| 37 | 36 | anassrs 467 |
. . . . . . . . 9
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → ((Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅)) |
| 38 | | predres 6360 |
. . . . . . . . . . . . . . . . 17
⊢
Pred(𝑅, 𝐵, 𝑦) = Pred((𝑅 ↾ 𝐵), 𝐵, 𝑦) |
| 39 | | predrelss 6358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 ↾ 𝐵) ⊆ t++(𝑅 ↾ 𝐵) → Pred((𝑅 ↾ 𝐵), 𝐵, 𝑦) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑦)) |
| 40 | 13, 39 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
Pred((𝑅 ↾
𝐵), 𝐵, 𝑦) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑦) |
| 41 | 38, 40 | eqsstri 4030 |
. . . . . . . . . . . . . . . 16
⊢
Pred(𝑅, 𝐵, 𝑦) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑦) |
| 42 | | inss1 4237 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵)) ⊆ t++(𝑅 ↾ 𝐵) |
| 43 | | coss1 5866 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((t++(𝑅 ↾
𝐵) ∩ (𝐵 × 𝐵)) ⊆ t++(𝑅 ↾ 𝐵) → ((t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵)) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) ⊆ (t++(𝑅 ↾ 𝐵) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵)))) |
| 44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
((t++(𝑅 ↾
𝐵) ∩ (𝐵 × 𝐵)) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) ⊆ (t++(𝑅 ↾ 𝐵) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) |
| 45 | | coss2 5867 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((t++(𝑅 ↾
𝐵) ∩ (𝐵 × 𝐵)) ⊆ t++(𝑅 ↾ 𝐵) → (t++(𝑅 ↾ 𝐵) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) ⊆ (t++(𝑅 ↾ 𝐵) ∘ t++(𝑅 ↾ 𝐵))) |
| 46 | 42, 45 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
⊢
(t++(𝑅 ↾ 𝐵) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) ⊆ (t++(𝑅 ↾ 𝐵) ∘ t++(𝑅 ↾ 𝐵)) |
| 47 | 44, 46 | sstri 3993 |
. . . . . . . . . . . . . . . . . 18
⊢
((t++(𝑅 ↾
𝐵) ∩ (𝐵 × 𝐵)) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) ⊆ (t++(𝑅 ↾ 𝐵) ∘ t++(𝑅 ↾ 𝐵)) |
| 48 | | ttrcltr 9756 |
. . . . . . . . . . . . . . . . . 18
⊢
(t++(𝑅 ↾ 𝐵) ∘ t++(𝑅 ↾ 𝐵)) ⊆ t++(𝑅 ↾ 𝐵) |
| 49 | 47, 48 | sstri 3993 |
. . . . . . . . . . . . . . . . 17
⊢
((t++(𝑅 ↾
𝐵) ∩ (𝐵 × 𝐵)) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) ⊆ t++(𝑅 ↾ 𝐵) |
| 50 | | predtrss 6343 |
. . . . . . . . . . . . . . . . 17
⊢
((((t++(𝑅 ↾
𝐵) ∩ (𝐵 × 𝐵)) ∘ (t++(𝑅 ↾ 𝐵) ∩ (𝐵 × 𝐵))) ⊆ t++(𝑅 ↾ 𝐵) ∧ 𝑦 ∈ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∧ 𝑏 ∈ 𝐵) → Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑦) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)) |
| 51 | 49, 50 | mp3an1 1450 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∧ 𝑏 ∈ 𝐵) → Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑦) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)) |
| 52 | 41, 51 | sstrid 3995 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∧ 𝑏 ∈ 𝐵) → Pred(𝑅, 𝐵, 𝑦) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)) |
| 53 | | sspred 6330 |
. . . . . . . . . . . . . . 15
⊢
((Pred(t++(𝑅 ↾
𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(𝑅, 𝐵, 𝑦) ⊆ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦)) |
| 54 | 19, 52, 53 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ∧ 𝑏 ∈ 𝐵) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦)) |
| 55 | 54 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦)) |
| 56 | 55 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑦 ∈ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)) → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅)) |
| 57 | 56 | rexbidva 3177 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐵 → (∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ ∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅)) |
| 58 | | ssrexv 4053 |
. . . . . . . . . . . 12
⊢
(Pred(t++(𝑅 ↾
𝐵), 𝐵, 𝑏) ⊆ 𝐵 → (∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 59 | 19, 58 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) |
| 60 | 57, 59 | biimtrrdi 254 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐵 → (∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 61 | 60 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → (∃𝑦 ∈ Pred (t++(𝑅 ↾ 𝐵), 𝐵, 𝑏)Pred(𝑅, Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 62 | 37, 61 | syld 47 |
. . . . . . . 8
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → ((Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(t++(𝑅 ↾ 𝐵), 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 63 | 20, 62 | syl5 34 |
. . . . . . 7
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 64 | 9, 63 | pm2.61dne 3028 |
. . . . . 6
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) |
| 65 | 64 | ex 412 |
. . . . 5
⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (𝑏 ∈ 𝐵 → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 66 | 65 | exlimdv 1933 |
. . . 4
⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (∃𝑏 𝑏 ∈ 𝐵 → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 67 | 4, 66 | biimtrid 242 |
. . 3
⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (𝐵 ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
| 68 | 3, 67 | syl6com 37 |
. 2
⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))) |
| 69 | 68 | imp32 418 |
1
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) |