| Step | Hyp | Ref
| Expression |
| 1 | | r19.2z 4495 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∃𝑥 ∈ 𝐴 𝑅 Er 𝐵) |
| 2 | | errel 8754 |
. . . . . 6
⊢ (𝑅 Er 𝐵 → Rel 𝑅) |
| 3 | | df-rel 5692 |
. . . . . 6
⊢ (Rel
𝑅 ↔ 𝑅 ⊆ (V × V)) |
| 4 | 2, 3 | sylib 218 |
. . . . 5
⊢ (𝑅 Er 𝐵 → 𝑅 ⊆ (V × V)) |
| 5 | 4 | reximi 3084 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 𝑅 Er 𝐵 → ∃𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
| 6 | | iinss 5056 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 𝑅 ⊆ (V × V) → ∩ 𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
| 7 | 1, 5, 6 | 3syl 18 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩
𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
| 8 | | df-rel 5692 |
. . 3
⊢ (Rel
∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∩
𝑥 ∈ 𝐴 𝑅 ⊆ (V × V)) |
| 9 | 7, 8 | sylibr 234 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → Rel ∩ 𝑥 ∈ 𝐴 𝑅) |
| 10 | | id 22 |
. . . . . . . . 9
⊢ (𝑅 Er 𝐵 → 𝑅 Er 𝐵) |
| 11 | 10 | ersymb 8759 |
. . . . . . . 8
⊢ (𝑅 Er 𝐵 → (𝑢𝑅𝑣 ↔ 𝑣𝑅𝑢)) |
| 12 | 11 | biimpd 229 |
. . . . . . 7
⊢ (𝑅 Er 𝐵 → (𝑢𝑅𝑣 → 𝑣𝑅𝑢)) |
| 13 | | df-br 5144 |
. . . . . . 7
⊢ (𝑢𝑅𝑣 ↔ 〈𝑢, 𝑣〉 ∈ 𝑅) |
| 14 | | df-br 5144 |
. . . . . . 7
⊢ (𝑣𝑅𝑢 ↔ 〈𝑣, 𝑢〉 ∈ 𝑅) |
| 15 | 12, 13, 14 | 3imtr3g 295 |
. . . . . 6
⊢ (𝑅 Er 𝐵 → (〈𝑢, 𝑣〉 ∈ 𝑅 → 〈𝑣, 𝑢〉 ∈ 𝑅)) |
| 16 | 15 | ral2imi 3085 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝑅 Er 𝐵 → (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 → ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅)) |
| 17 | 16 | adantl 481 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 → ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅)) |
| 18 | | df-br 5144 |
. . . . 5
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ↔ 〈𝑢, 𝑣〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
| 19 | | opex 5469 |
. . . . . 6
⊢
〈𝑢, 𝑣〉 ∈ V |
| 20 | | eliin 4996 |
. . . . . 6
⊢
(〈𝑢, 𝑣〉 ∈ V →
(〈𝑢, 𝑣〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅)) |
| 21 | 19, 20 | ax-mp 5 |
. . . . 5
⊢
(〈𝑢, 𝑣〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅) |
| 22 | 18, 21 | bitri 275 |
. . . 4
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅) |
| 23 | | df-br 5144 |
. . . . 5
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ 〈𝑣, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
| 24 | | opex 5469 |
. . . . . 6
⊢
〈𝑣, 𝑢〉 ∈ V |
| 25 | | eliin 4996 |
. . . . . 6
⊢
(〈𝑣, 𝑢〉 ∈ V →
(〈𝑣, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅)) |
| 26 | 24, 25 | ax-mp 5 |
. . . . 5
⊢
(〈𝑣, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅) |
| 27 | 23, 26 | bitri 275 |
. . . 4
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑢〉 ∈ 𝑅) |
| 28 | 17, 22, 27 | 3imtr4g 296 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 → 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢)) |
| 29 | 28 | imp 406 |
. 2
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) ∧ 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣) → 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑢) |
| 30 | | r19.26 3111 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) ↔ (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅)) |
| 31 | 10 | ertr 8760 |
. . . . . . . 8
⊢ (𝑅 Er 𝐵 → ((𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤) → 𝑢𝑅𝑤)) |
| 32 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝑣𝑅𝑤 ↔ 〈𝑣, 𝑤〉 ∈ 𝑅) |
| 33 | 13, 32 | anbi12i 628 |
. . . . . . . 8
⊢ ((𝑢𝑅𝑣 ∧ 𝑣𝑅𝑤) ↔ (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅)) |
| 34 | | df-br 5144 |
. . . . . . . 8
⊢ (𝑢𝑅𝑤 ↔ 〈𝑢, 𝑤〉 ∈ 𝑅) |
| 35 | 31, 33, 34 | 3imtr3g 295 |
. . . . . . 7
⊢ (𝑅 Er 𝐵 → ((〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) → 〈𝑢, 𝑤〉 ∈ 𝑅)) |
| 36 | 35 | ral2imi 3085 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 𝑅 Er 𝐵 → (∀𝑥 ∈ 𝐴 (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
| 37 | 36 | adantl 481 |
. . . . 5
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (∀𝑥 ∈ 𝐴 (〈𝑢, 𝑣〉 ∈ 𝑅 ∧ 〈𝑣, 𝑤〉 ∈ 𝑅) → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
| 38 | 30, 37 | biimtrrid 243 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ((∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅) → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
| 39 | | df-br 5144 |
. . . . . 6
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ 〈𝑣, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
| 40 | | opex 5469 |
. . . . . . 7
⊢
〈𝑣, 𝑤〉 ∈ V |
| 41 | | eliin 4996 |
. . . . . . 7
⊢
(〈𝑣, 𝑤〉 ∈ V →
(〈𝑣, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅)) |
| 42 | 40, 41 | ax-mp 5 |
. . . . . 6
⊢
(〈𝑣, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅) |
| 43 | 39, 42 | bitri 275 |
. . . . 5
⊢ (𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅) |
| 44 | 22, 43 | anbi12i 628 |
. . . 4
⊢ ((𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ∧ 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤) ↔ (∀𝑥 ∈ 𝐴 〈𝑢, 𝑣〉 ∈ 𝑅 ∧ ∀𝑥 ∈ 𝐴 〈𝑣, 𝑤〉 ∈ 𝑅)) |
| 45 | | df-br 5144 |
. . . . 5
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ 〈𝑢, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
| 46 | | opex 5469 |
. . . . . 6
⊢
〈𝑢, 𝑤〉 ∈ V |
| 47 | | eliin 4996 |
. . . . . 6
⊢
(〈𝑢, 𝑤〉 ∈ V →
(〈𝑢, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅)) |
| 48 | 46, 47 | ax-mp 5 |
. . . . 5
⊢
(〈𝑢, 𝑤〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅) |
| 49 | 45, 48 | bitri 275 |
. . . 4
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑤〉 ∈ 𝑅) |
| 50 | 38, 44, 49 | 3imtr4g 296 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ((𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ∧ 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤) → 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤)) |
| 51 | 50 | imp 406 |
. 2
⊢ (((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) ∧ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑣 ∧ 𝑣∩ 𝑥 ∈ 𝐴 𝑅𝑤)) → 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑤) |
| 52 | | simpl 482 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 𝑅 Er 𝐵) |
| 53 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 𝑢 ∈ 𝐵) |
| 54 | 52, 53 | erref 8765 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 𝑢𝑅𝑢) |
| 55 | | df-br 5144 |
. . . . . . . . 9
⊢ (𝑢𝑅𝑢 ↔ 〈𝑢, 𝑢〉 ∈ 𝑅) |
| 56 | 54, 55 | sylib 218 |
. . . . . . . 8
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ 𝐵) → 〈𝑢, 𝑢〉 ∈ 𝑅) |
| 57 | 56 | expcom 413 |
. . . . . . 7
⊢ (𝑢 ∈ 𝐵 → (𝑅 Er 𝐵 → 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 58 | 57 | ralimdv 3169 |
. . . . . 6
⊢ (𝑢 ∈ 𝐵 → (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 59 | 58 | com12 32 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝑅 Er 𝐵 → (𝑢 ∈ 𝐵 → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 60 | 59 | adantl 481 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢 ∈ 𝐵 → ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 61 | | r19.26 3111 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) ↔ (∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 ∧ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 62 | | r19.2z 4495 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅)) → ∃𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 63 | | vex 3484 |
. . . . . . . . . . 11
⊢ 𝑢 ∈ V |
| 64 | 63, 63 | opeldm 5918 |
. . . . . . . . . 10
⊢
(〈𝑢, 𝑢〉 ∈ 𝑅 → 𝑢 ∈ dom 𝑅) |
| 65 | | erdm 8755 |
. . . . . . . . . . . 12
⊢ (𝑅 Er 𝐵 → dom 𝑅 = 𝐵) |
| 66 | 65 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (𝑅 Er 𝐵 → (𝑢 ∈ dom 𝑅 ↔ 𝑢 ∈ 𝐵)) |
| 67 | 66 | biimpa 476 |
. . . . . . . . . 10
⊢ ((𝑅 Er 𝐵 ∧ 𝑢 ∈ dom 𝑅) → 𝑢 ∈ 𝐵) |
| 68 | 64, 67 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵) |
| 69 | 68 | rexlimivw 3151 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵) |
| 70 | 62, 69 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅)) → 𝑢 ∈ 𝐵) |
| 71 | 70 | ex 412 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 (𝑅 Er 𝐵 ∧ 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵)) |
| 72 | 61, 71 | biimtrrid 243 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
((∀𝑥 ∈ 𝐴 𝑅 Er 𝐵 ∧ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅) → 𝑢 ∈ 𝐵)) |
| 73 | 72 | expdimp 452 |
. . . 4
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅 → 𝑢 ∈ 𝐵)) |
| 74 | 60, 73 | impbid 212 |
. . 3
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 75 | | df-br 5144 |
. . . 4
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ 〈𝑢, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅) |
| 76 | | opex 5469 |
. . . . 5
⊢
〈𝑢, 𝑢〉 ∈ V |
| 77 | | eliin 4996 |
. . . . 5
⊢
(〈𝑢, 𝑢〉 ∈ V →
(〈𝑢, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅)) |
| 78 | 76, 77 | ax-mp 5 |
. . . 4
⊢
(〈𝑢, 𝑢〉 ∈ ∩ 𝑥 ∈ 𝐴 𝑅 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅) |
| 79 | 75, 78 | bitri 275 |
. . 3
⊢ (𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑢 ↔ ∀𝑥 ∈ 𝐴 〈𝑢, 𝑢〉 ∈ 𝑅) |
| 80 | 74, 79 | bitr4di 289 |
. 2
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → (𝑢 ∈ 𝐵 ↔ 𝑢∩ 𝑥 ∈ 𝐴 𝑅𝑢)) |
| 81 | 9, 29, 51, 80 | iserd 8771 |
1
⊢ ((𝐴 ≠ ∅ ∧
∀𝑥 ∈ 𝐴 𝑅 Er 𝐵) → ∩
𝑥 ∈ 𝐴 𝑅 Er 𝐵) |