Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . . . 6
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
2 | | predel 6217 |
. . . . . . . 8
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴) |
3 | 2 | 3ad2ant2 1133 |
. . . . . . 7
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → 𝑌 ∈ 𝐴) |
4 | 3 | adantr 481 |
. . . . . 6
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑌 ∈ 𝐴) |
5 | | brxp 5632 |
. . . . . 6
⊢ (𝑧(𝐴 × 𝐴)𝑌 ↔ (𝑧 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) |
6 | 1, 4, 5 | sylanbrc 583 |
. . . . 5
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑧(𝐴 × 𝐴)𝑌) |
7 | | brin 5126 |
. . . . . 6
⊢ (𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 ↔ (𝑧𝑅𝑌 ∧ 𝑧(𝐴 × 𝐴)𝑌)) |
8 | | predbrg 6218 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋) |
9 | 8 | ancoms 459 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → 𝑌𝑅𝑋) |
10 | 9 | 3adant1 1129 |
. . . . . . . . 9
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → 𝑌𝑅𝑋) |
11 | 10 | adantr 481 |
. . . . . . . 8
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑌𝑅𝑋) |
12 | | simpl3 1192 |
. . . . . . . . 9
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑋 ∈ 𝐴) |
13 | | brxp 5632 |
. . . . . . . . 9
⊢ (𝑌(𝐴 × 𝐴)𝑋 ↔ (𝑌 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴)) |
14 | 4, 12, 13 | sylanbrc 583 |
. . . . . . . 8
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑌(𝐴 × 𝐴)𝑋) |
15 | | brin 5126 |
. . . . . . . 8
⊢ (𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋 ↔ (𝑌𝑅𝑋 ∧ 𝑌(𝐴 × 𝐴)𝑋)) |
16 | 11, 14, 15 | sylanbrc 583 |
. . . . . . 7
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋) |
17 | | breq2 5078 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ 𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌)) |
18 | | breq1 5077 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑌 → (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑋 ↔ 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋)) |
19 | 17, 18 | anbi12d 631 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑌 → ((𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑋) ↔ (𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 ∧ 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋))) |
20 | 19 | spcegv 3534 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → ((𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 ∧ 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋) → ∃𝑦(𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑋))) |
21 | 20 | 3ad2ant2 1133 |
. . . . . . . . . 10
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → ((𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 ∧ 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋) → ∃𝑦(𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑋))) |
22 | 21 | adantr 481 |
. . . . . . . . 9
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 ∧ 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋) → ∃𝑦(𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑋))) |
23 | | vex 3434 |
. . . . . . . . . 10
⊢ 𝑧 ∈ V |
24 | | brcog 5769 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ V ∧ 𝑋 ∈ 𝐴) → (𝑧((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑋 ↔ ∃𝑦(𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑋))) |
25 | 23, 12, 24 | sylancr 587 |
. . . . . . . . 9
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑋 ↔ ∃𝑦(𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑋))) |
26 | 22, 25 | sylibrd 258 |
. . . . . . . 8
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 ∧ 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋) → 𝑧((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑋)) |
27 | | simpl1 1190 |
. . . . . . . . 9
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) |
28 | 27 | ssbrd 5117 |
. . . . . . . 8
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑋 → 𝑧𝑅𝑋)) |
29 | 26, 28 | syld 47 |
. . . . . . 7
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 ∧ 𝑌(𝑅 ∩ (𝐴 × 𝐴))𝑋) → 𝑧𝑅𝑋)) |
30 | 16, 29 | mpan2d 691 |
. . . . . 6
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧(𝑅 ∩ (𝐴 × 𝐴))𝑌 → 𝑧𝑅𝑋)) |
31 | 7, 30 | syl5bir 242 |
. . . . 5
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝑧𝑅𝑌 ∧ 𝑧(𝐴 × 𝐴)𝑌) → 𝑧𝑅𝑋)) |
32 | 6, 31 | mpan2d 691 |
. . . 4
⊢
(((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → (𝑧𝑅𝑌 → 𝑧𝑅𝑋)) |
33 | 32 | imdistanda 572 |
. . 3
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → ((𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑌) → (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑋))) |
34 | 23 | elpred 6213 |
. . . 4
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑌) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑌))) |
35 | 34 | 3ad2ant2 1133 |
. . 3
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑌) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑌))) |
36 | 23 | elpred 6213 |
. . . 4
⊢ (𝑋 ∈ 𝐴 → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑋))) |
37 | 36 | 3ad2ant3 1134 |
. . 3
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑧 ∈ 𝐴 ∧ 𝑧𝑅𝑋))) |
38 | 33, 35, 37 | 3imtr4d 294 |
. 2
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → (𝑧 ∈ Pred(𝑅, 𝐴, 𝑌) → 𝑧 ∈ Pred(𝑅, 𝐴, 𝑋))) |
39 | 38 | ssrdv 3927 |
1
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)) |