Step | Hyp | Ref
| Expression |
1 | | predel 6157 |
. 2
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴) |
2 | | elpredg 6154 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋)) |
3 | 2 | adantll 714 |
. . . . . . . . . 10
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋)) |
4 | | potr 5466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Po 𝐴 ∧ (𝑧 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝑧𝑅𝑌 ∧ 𝑌𝑅𝑋) → 𝑧𝑅𝑋)) |
5 | 4 | 3exp2 1356 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Po 𝐴 → (𝑧 ∈ 𝐴 → (𝑌 ∈ 𝐴 → (𝑋 ∈ 𝐴 → ((𝑧𝑅𝑌 ∧ 𝑌𝑅𝑋) → 𝑧𝑅𝑋))))) |
6 | 5 | com24 95 |
. . . . . . . . . . . . . 14
⊢ (𝑅 Po 𝐴 → (𝑋 ∈ 𝐴 → (𝑌 ∈ 𝐴 → (𝑧 ∈ 𝐴 → ((𝑧𝑅𝑌 ∧ 𝑌𝑅𝑋) → 𝑧𝑅𝑋))))) |
7 | 6 | imp31 421 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ 𝐴) → (𝑧 ∈ 𝐴 → ((𝑧𝑅𝑌 ∧ 𝑌𝑅𝑋) → 𝑧𝑅𝑋))) |
8 | 7 | com13 88 |
. . . . . . . . . . . 12
⊢ ((𝑧𝑅𝑌 ∧ 𝑌𝑅𝑋) → (𝑧 ∈ 𝐴 → (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ 𝐴) → 𝑧𝑅𝑋))) |
9 | 8 | ex 416 |
. . . . . . . . . . 11
⊢ (𝑧𝑅𝑌 → (𝑌𝑅𝑋 → (𝑧 ∈ 𝐴 → (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ 𝐴) → 𝑧𝑅𝑋)))) |
10 | 9 | com14 96 |
. . . . . . . . . 10
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ 𝐴) → (𝑌𝑅𝑋 → (𝑧 ∈ 𝐴 → (𝑧𝑅𝑌 → 𝑧𝑅𝑋)))) |
11 | 3, 10 | sylbid 243 |
. . . . . . . . 9
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → (𝑧 ∈ 𝐴 → (𝑧𝑅𝑌 → 𝑧𝑅𝑋)))) |
12 | 11 | ex 416 |
. . . . . . . 8
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ 𝐴 → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → (𝑧 ∈ 𝐴 → (𝑧𝑅𝑌 → 𝑧𝑅𝑋))))) |
13 | 12 | com23 86 |
. . . . . . 7
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → (𝑌 ∈ 𝐴 → (𝑧 ∈ 𝐴 → (𝑧𝑅𝑌 → 𝑧𝑅𝑋))))) |
14 | 13 | 3imp 1113 |
. . . . . 6
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑌 ∈ 𝐴) → (𝑧 ∈ 𝐴 → (𝑧𝑅𝑌 → 𝑧𝑅𝑋))) |
15 | 14 | imdistand 574 |
. . . . 5
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑌 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑌) → (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑋))) |
16 | | vex 3402 |
. . . . . . 7
⊢ 𝑧 ∈ V |
17 | 16 | elpred 6153 |
. . . . . 6
⊢ (𝑌 ∈ 𝐴 → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑌) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑌))) |
18 | 17 | 3ad2ant3 1137 |
. . . . 5
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑌 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑌) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑌))) |
19 | 16 | elpred 6153 |
. . . . . . 7
⊢ (𝑋 ∈ 𝐴 → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑋))) |
20 | 19 | adantl 485 |
. . . . . 6
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑋))) |
21 | 20 | 3ad2ant1 1135 |
. . . . 5
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑌 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑋))) |
22 | 15, 18, 21 | 3imtr4d 297 |
. . . 4
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑌 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑌) → 𝑧 ∈ Pred(𝑅, 𝐴, 𝑋))) |
23 | 22 | ssrdv 3893 |
. . 3
⊢ (((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑌 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)) |
24 | 23 | 3exp 1121 |
. 2
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → (𝑌 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)))) |
25 | 1, 24 | mpdi 45 |
1
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))) |