Step | Hyp | Ref
| Expression |
1 | | frss 5518 |
. . . 4
⊢ (𝐵 ⊆ 𝐴 → (𝑅 Fr 𝐴 → 𝑅 Fr 𝐵)) |
2 | | sess2 5520 |
. . . 4
⊢ (𝐵 ⊆ 𝐴 → (𝑅 Se 𝐴 → 𝑅 Se 𝐵)) |
3 | 1, 2 | anim12d 612 |
. . 3
⊢ (𝐵 ⊆ 𝐴 → ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → (𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵))) |
4 | | n0 4261 |
. . . 4
⊢ (𝐵 ≠ ∅ ↔
∃𝑏 𝑏 ∈ 𝐵) |
5 | | predeq3 6164 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑏 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐵, 𝑏)) |
6 | 5 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, 𝐵, 𝑏) = ∅)) |
7 | 6 | rspcev 3537 |
. . . . . . . . 9
⊢ ((𝑏 ∈ 𝐵 ∧ Pred(𝑅, 𝐵, 𝑏) = ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) |
8 | 7 | ex 416 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
9 | 8 | adantl 485 |
. . . . . . 7
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → (Pred(𝑅, 𝐵, 𝑏) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
10 | | setlikespec 6183 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → Pred(𝑅, 𝐵, 𝑏) ∈ V) |
11 | | trpredpred 9333 |
. . . . . . . . . . . . 13
⊢
(Pred(𝑅, 𝐵, 𝑏) ∈ V → Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏)) |
12 | | ssn0 4315 |
. . . . . . . . . . . . . 14
⊢
((Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏) ∧ Pred(𝑅, 𝐵, 𝑏) ≠ ∅) → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) |
13 | 12 | ex 416 |
. . . . . . . . . . . . 13
⊢
(Pred(𝑅, 𝐵, 𝑏) ⊆ TrPred(𝑅, 𝐵, 𝑏) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)) |
14 | 11, 13 | syl 17 |
. . . . . . . . . . . 12
⊢
(Pred(𝑅, 𝐵, 𝑏) ∈ V → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)) |
15 | | trpredss 9334 |
. . . . . . . . . . . 12
⊢
(Pred(𝑅, 𝐵, 𝑏) ∈ V → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵) |
16 | 14, 15 | jctild 529 |
. . . . . . . . . . 11
⊢
(Pred(𝑅, 𝐵, 𝑏) ∈ V → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))) |
17 | 10, 16 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))) |
18 | 17 | adantr 484 |
. . . . . . . . 9
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))) |
19 | | trpredex 9343 |
. . . . . . . . . . 11
⊢
TrPred(𝑅, 𝐵, 𝑏) ∈ V |
20 | | sseq1 3926 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (𝑐 ⊆ 𝐵 ↔ TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵)) |
21 | | neeq1 3003 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (𝑐 ≠ ∅ ↔ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅)) |
22 | 20, 21 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) ↔ (TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅))) |
23 | | predeq2 6163 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → Pred(𝑅, 𝑐, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦)) |
24 | 23 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅)) |
25 | 24 | rexeqbi1dv 3318 |
. . . . . . . . . . . . 13
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅ ↔ ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅)) |
26 | 22, 25 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → (((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) ↔ ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅))) |
27 | 26 | imbi2d 344 |
. . . . . . . . . . 11
⊢ (𝑐 = TrPred(𝑅, 𝐵, 𝑏) → ((𝑅 Fr 𝐵 → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) ↔ (𝑅 Fr 𝐵 → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅)))) |
28 | | dffr4 6178 |
. . . . . . . . . . . 12
⊢ (𝑅 Fr 𝐵 ↔ ∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) |
29 | | sp 2180 |
. . . . . . . . . . . 12
⊢
(∀𝑐((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅) → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) |
30 | 28, 29 | sylbi 220 |
. . . . . . . . . . 11
⊢ (𝑅 Fr 𝐵 → ((𝑐 ⊆ 𝐵 ∧ 𝑐 ≠ ∅) → ∃𝑦 ∈ 𝑐 Pred(𝑅, 𝑐, 𝑦) = ∅)) |
31 | 19, 27, 30 | vtocl 3474 |
. . . . . . . . . 10
⊢ (𝑅 Fr 𝐵 → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅)) |
32 | 10, 15 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵) |
33 | 32 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵) |
34 | | trpredtr 9335 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏) → Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏))) |
35 | 34 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏)) |
36 | | sspred 6168 |
. . . . . . . . . . . . . . 15
⊢
((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ Pred(𝑅, 𝐵, 𝑦) ⊆ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦)) |
37 | 33, 35, 36 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦)) |
38 | 37 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → (Pred(𝑅, 𝐵, 𝑦) = ∅ ↔ Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅)) |
39 | 38 | biimprd 251 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑦 ∈ TrPred(𝑅, 𝐵, 𝑏)) → (Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → Pred(𝑅, 𝐵, 𝑦) = ∅)) |
40 | 39 | reximdva 3193 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅)) |
41 | | ssrexv 3968 |
. . . . . . . . . . 11
⊢
(TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, 𝐵, 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
42 | 32, 40, 41 | sylsyld 61 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) → (∃𝑦 ∈ TrPred (𝑅, 𝐵, 𝑏)Pred(𝑅, TrPred(𝑅, 𝐵, 𝑏), 𝑦) = ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
43 | 31, 42 | sylan9r 512 |
. . . . . . . . 9
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → ((TrPred(𝑅, 𝐵, 𝑏) ⊆ 𝐵 ∧ TrPred(𝑅, 𝐵, 𝑏) ≠ ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
44 | 18, 43 | syld 47 |
. . . . . . . 8
⊢ (((𝑏 ∈ 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑅 Fr 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
45 | 44 | an31s 654 |
. . . . . . 7
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → (Pred(𝑅, 𝐵, 𝑏) ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
46 | 9, 45 | pm2.61dne 3028 |
. . . . . 6
⊢ (((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) ∧ 𝑏 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) |
47 | 46 | ex 416 |
. . . . 5
⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (𝑏 ∈ 𝐵 → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
48 | 47 | exlimdv 1941 |
. . . 4
⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (∃𝑏 𝑏 ∈ 𝐵 → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
49 | 4, 48 | syl5bi 245 |
. . 3
⊢ ((𝑅 Fr 𝐵 ∧ 𝑅 Se 𝐵) → (𝐵 ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅)) |
50 | 3, 49 | syl6com 37 |
. 2
⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → (𝐵 ⊆ 𝐴 → (𝐵 ≠ ∅ → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅))) |
51 | 50 | imp32 422 |
1
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) |