Step |
Hyp |
Ref |
Expression |
1 |
|
predel |
⊢ ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → 𝑌 ∈ 𝐴 ) |
2 |
|
elpredg |
⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) ) |
3 |
2
|
adantll |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ 𝑌 𝑅 𝑋 ) ) |
4 |
|
potr |
⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴 ) ) → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) ) |
5 |
4
|
3exp2 |
⊢ ( 𝑅 Po 𝐴 → ( 𝑧 ∈ 𝐴 → ( 𝑌 ∈ 𝐴 → ( 𝑋 ∈ 𝐴 → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) ) ) ) ) |
6 |
5
|
com24 |
⊢ ( 𝑅 Po 𝐴 → ( 𝑋 ∈ 𝐴 → ( 𝑌 ∈ 𝐴 → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) ) ) ) ) |
7 |
6
|
imp31 |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐴 → ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → 𝑧 𝑅 𝑋 ) ) ) |
8 |
7
|
com13 |
⊢ ( ( 𝑧 𝑅 𝑌 ∧ 𝑌 𝑅 𝑋 ) → ( 𝑧 ∈ 𝐴 → ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → 𝑧 𝑅 𝑋 ) ) ) |
9 |
8
|
ex |
⊢ ( 𝑧 𝑅 𝑌 → ( 𝑌 𝑅 𝑋 → ( 𝑧 ∈ 𝐴 → ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → 𝑧 𝑅 𝑋 ) ) ) ) |
10 |
9
|
com14 |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 𝑅 𝑋 → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) ) |
11 |
3 10
|
sylbid |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) ) |
12 |
11
|
ex |
⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ 𝐴 → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) ) ) |
13 |
12
|
com23 |
⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑌 ∈ 𝐴 → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) ) ) |
14 |
13
|
3imp |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 𝑅 𝑌 → 𝑧 𝑅 𝑋 ) ) ) |
15 |
14
|
imdistand |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) → ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) ) |
16 |
|
vex |
⊢ 𝑧 ∈ V |
17 |
16
|
elpred |
⊢ ( 𝑌 ∈ 𝐴 → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) ) ) |
18 |
17
|
3ad2ant3 |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑌 ) ) ) |
19 |
16
|
elpred |
⊢ ( 𝑋 ∈ 𝐴 → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) ) |
20 |
19
|
adantl |
⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) ) |
21 |
20
|
3ad2ant1 |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 𝑅 𝑋 ) ) ) |
22 |
15 18 21
|
3imtr4d |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑌 ) → 𝑧 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) |
23 |
22
|
ssrdv |
⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) ∧ 𝑌 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) |
24 |
23
|
3exp |
⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → ( 𝑌 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) ) |
25 |
1 24
|
mpdi |
⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑌 ∈ Pred ( 𝑅 , 𝐴 , 𝑋 ) → Pred ( 𝑅 , 𝐴 , 𝑌 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑋 ) ) ) |