Step | Hyp | Ref
| Expression |
1 | | eleq1 2689 |
. . . . 5
⊢ (𝑦 = 𝑋 → (𝑦 ∈ 𝐵 ↔ 𝑋 ∈ 𝐵)) |
2 | | predeq3 5684 |
. . . . . 6
⊢ (𝑦 = 𝑋 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐵, 𝑋)) |
3 | | predeq3 5684 |
. . . . . 6
⊢ (𝑦 = 𝑋 → Pred(𝑅, 𝐴, 𝑦) = Pred(𝑅, 𝐴, 𝑋)) |
4 | 2, 3 | eqeq12d 2637 |
. . . . 5
⊢ (𝑦 = 𝑋 → (Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦) ↔ Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) |
5 | 1, 4 | imbi12d 334 |
. . . 4
⊢ (𝑦 = 𝑋 → ((𝑦 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦)) ↔ (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋)))) |
6 | 5 | imbi2d 330 |
. . 3
⊢ (𝑦 = 𝑋 → (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦))) ↔ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))))) |
7 | | predpredss 5686 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 → Pred(𝑅, 𝐵, 𝑦) ⊆ Pred(𝑅, 𝐴, 𝑦)) |
8 | 7 | ad2antrr 762 |
. . . . 5
⊢ (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐵, 𝑦) ⊆ Pred(𝑅, 𝐴, 𝑦)) |
9 | | predeq3 5684 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → Pred(𝑅, 𝐴, 𝑥) = Pred(𝑅, 𝐴, 𝑦)) |
10 | 9 | sseq1d 3632 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ↔ Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵)) |
11 | 10 | rspccva 3308 |
. . . . . . . . . 10
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵) |
12 | 11 | sseld 3602 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ 𝐵)) |
13 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
14 | 13 | elpredim 5692 |
. . . . . . . . . 10
⊢ (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧𝑅𝑦) |
15 | 14 | a1i 11 |
. . . . . . . . 9
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧𝑅𝑦)) |
16 | 12, 15 | jcad 555 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦))) |
17 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑧 ∈ V |
18 | 17 | elpred 5693 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐵 → (𝑧 ∈ Pred(𝑅, 𝐵, 𝑦) ↔ (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦))) |
19 | 18 | imbi2d 330 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐵 → ((𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ Pred(𝑅, 𝐵, 𝑦)) ↔ (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦)))) |
20 | 19 | adantl 482 |
. . . . . . . 8
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → ((𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ Pred(𝑅, 𝐵, 𝑦)) ↔ (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → (𝑧 ∈ 𝐵 ∧ 𝑧𝑅𝑦)))) |
21 | 16, 20 | mpbird 247 |
. . . . . . 7
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑦) → 𝑧 ∈ Pred(𝑅, 𝐵, 𝑦))) |
22 | 21 | ssrdv 3609 |
. . . . . 6
⊢
((∀𝑥 ∈
𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵 ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐴, 𝑦) ⊆ Pred(𝑅, 𝐵, 𝑦)) |
23 | 22 | adantll 750 |
. . . . 5
⊢ (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐴, 𝑦) ⊆ Pred(𝑅, 𝐵, 𝑦)) |
24 | 8, 23 | eqssd 3620 |
. . . 4
⊢ (((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) ∧ 𝑦 ∈ 𝐵) → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦)) |
25 | 24 | ex 450 |
. . 3
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑦 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑦) = Pred(𝑅, 𝐴, 𝑦))) |
26 | 6, 25 | vtoclg 3266 |
. 2
⊢ (𝑋 ∈ 𝐵 → ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋)))) |
27 | 26 | pm2.43b 55 |
1
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) |