Step | Hyp | Ref
| Expression |
1 | | eleq1 2825 |
. . . . 5
⊢ (𝑦 = 𝑋 → (𝑦 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵)) |
2 | | predeq3 6164 |
. . . . . 6
⊢ (𝑦 = 𝑋 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐵, 𝑋)) |
3 | | predeq3 6164 |
. . . . . 6
⊢ (𝑦 = 𝑋 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑋)) |
4 | 2, 3 | eqeq12d 2753 |
. . . . 5
⊢ (𝑦 = 𝑋 → (Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦) ↔ Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) |
5 | 1, 4 | imbi12d 348 |
. . . 4
⊢ (𝑦 = 𝑋 → ((𝑦 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦)) ↔ (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋)))) |
6 | 5 | imbi2d 344 |
. . 3
⊢ (𝑦 = 𝑋 → (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦))) ↔ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))))) |
7 | | predpredss 6166 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 → Pred(𝑅, 𝐵, 𝑦) ⊆ Pred(𝑅, 𝐴, 𝑦)) |
8 | 7 | ad2antrr 726 |
. . . . 5
⊢ (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐵, 𝑦) ⊆ Pred(𝑅, 𝐴, 𝑦)) |
9 | | predeq3 6164 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → Pred(𝑅, 𝐴, 𝑥) = Pred(𝑅, 𝐴, 𝑦)) |
10 | 9 | sseq1d 3932 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ↔ Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)) |
11 | 10 | rspccva 3536 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵) |
12 | 11 | sseld 3900 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ 𝐵)) |
13 | | vex 3412 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
14 | 13 | elpredim 6175 |
. . . . . . . . 9
⊢ (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧𝑅𝑦) |
15 | 12, 14 | jca2 517 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦))) |
16 | | vex 3412 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
17 | 16 | elpred 6176 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → (𝑧 ∈ Pred(𝑅, 𝐵, 𝑦) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦))) |
18 | 17 | imbi2d 344 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → ((𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ Pred(𝑅, 𝐵, 𝑦)) ↔ (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦)))) |
19 | 18 | adantl 485 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ Pred(𝑅, 𝐵, 𝑦)) ↔ (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦)))) |
20 | 15, 19 | mpbird 260 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ Pred(𝑅, 𝐵, 𝑦))) |
21 | 20 | ssrdv 3907 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐴, 𝑦) ⊆ Pred(𝑅, 𝐵, 𝑦)) |
22 | 21 | adantll 714 |
. . . . 5
⊢ (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐴, 𝑦) ⊆ Pred(𝑅, 𝐵, 𝑦)) |
23 | 8, 22 | eqssd 3918 |
. . . 4
⊢ (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦)) |
24 | 23 | ex 416 |
. . 3
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦))) |
25 | 6, 24 | vtoclg 3481 |
. 2
⊢ (𝑋 ∈ 𝐵 → ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋)))) |
26 | 25 | pm2.43b 55 |
1
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) |