| Step | Hyp | Ref
| Expression |
| 1 | | df-xrn 38372 |
. . . 4
⊢ (𝑅 ⋉ 𝑆) = ((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆)) |
| 2 | 1 | breqi 5149 |
. . 3
⊢ (𝐴(𝑅 ⋉ 𝑆)〈𝐵, 𝐶〉 ↔ 𝐴((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆))〈𝐵, 𝐶〉) |
| 3 | 2 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)〈𝐵, 𝐶〉 ↔ 𝐴((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆))〈𝐵, 𝐶〉)) |
| 4 | | brin 5195 |
. . 3
⊢ (𝐴((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆))〈𝐵, 𝐶〉 ↔ (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)〈𝐵, 𝐶〉 ∧ 𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)〈𝐵, 𝐶〉)) |
| 5 | 4 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆))〈𝐵, 𝐶〉 ↔ (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)〈𝐵, 𝐶〉 ∧ 𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)〈𝐵, 𝐶〉))) |
| 6 | | opex 5469 |
. . . . . 6
⊢
〈𝐵, 𝐶〉 ∈ V |
| 7 | | brcog 5877 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 〈𝐵, 𝐶〉 ∈ V) → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)〈𝐵, 𝐶〉 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉))) |
| 8 | 6, 7 | mpan2 691 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)〈𝐵, 𝐶〉 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉))) |
| 9 | 8 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)〈𝐵, 𝐶〉 ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉))) |
| 10 | | brcnvg 5890 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 〈𝐵, 𝐶〉 ∈ V) → (𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 〈𝐵, 𝐶〉(1st ↾ (V ×
V))𝑥)) |
| 11 | 6, 10 | mpan2 691 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 〈𝐵, 𝐶〉(1st ↾ (V ×
V))𝑥)) |
| 12 | 11 | elv 3485 |
. . . . . . 7
⊢ (𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 〈𝐵, 𝐶〉(1st ↾ (V ×
V))𝑥) |
| 13 | | brres 6004 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ V → (〈𝐵, 𝐶〉(1st ↾ (V ×
V))𝑥 ↔ (〈𝐵, 𝐶〉 ∈ (V × V) ∧
〈𝐵, 𝐶〉1st 𝑥))) |
| 14 | 13 | elv 3485 |
. . . . . . . . . 10
⊢
(〈𝐵, 𝐶〉(1st ↾ (V
× V))𝑥 ↔
(〈𝐵, 𝐶〉 ∈ (V × V) ∧
〈𝐵, 𝐶〉1st 𝑥)) |
| 15 | | opelvvg 5726 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → 〈𝐵, 𝐶〉 ∈ (V ×
V)) |
| 16 | 15 | biantrurd 532 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉1st 𝑥 ↔ (〈𝐵, 𝐶〉 ∈ (V × V) ∧
〈𝐵, 𝐶〉1st 𝑥))) |
| 17 | 14, 16 | bitr4id 290 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉(1st ↾ (V ×
V))𝑥 ↔ 〈𝐵, 𝐶〉1st 𝑥)) |
| 18 | | br1steqg 8036 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉1st 𝑥 ↔ 𝑥 = 𝐵)) |
| 19 | 17, 18 | bitrd 279 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉(1st ↾ (V ×
V))𝑥 ↔ 𝑥 = 𝐵)) |
| 20 | 19 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉(1st ↾ (V ×
V))𝑥 ↔ 𝑥 = 𝐵)) |
| 21 | 12, 20 | bitrid 283 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 𝑥 = 𝐵)) |
| 22 | 21 | anbi1cd 635 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉) ↔ (𝑥 = 𝐵 ∧ 𝐴𝑅𝑥))) |
| 23 | 22 | exbidv 1921 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))〈𝐵, 𝐶〉) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴𝑅𝑥))) |
| 24 | | breq2 5147 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) |
| 25 | 24 | ceqsexgv 3654 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → (∃𝑥(𝑥 = 𝐵 ∧ 𝐴𝑅𝑥) ↔ 𝐴𝑅𝐵)) |
| 26 | 25 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥(𝑥 = 𝐵 ∧ 𝐴𝑅𝑥) ↔ 𝐴𝑅𝐵)) |
| 27 | 9, 23, 26 | 3bitrd 305 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)〈𝐵, 𝐶〉 ↔ 𝐴𝑅𝐵)) |
| 28 | | brcog 5877 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 〈𝐵, 𝐶〉 ∈ V) → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)〈𝐵, 𝐶〉 ↔ ∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉))) |
| 29 | 6, 28 | mpan2 691 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)〈𝐵, 𝐶〉 ↔ ∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉))) |
| 30 | 29 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)〈𝐵, 𝐶〉 ↔ ∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉))) |
| 31 | | brcnvg 5890 |
. . . . . . . . 9
⊢ ((𝑦 ∈ V ∧ 〈𝐵, 𝐶〉 ∈ V) → (𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 〈𝐵, 𝐶〉(2nd ↾ (V ×
V))𝑦)) |
| 32 | 6, 31 | mpan2 691 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 〈𝐵, 𝐶〉(2nd ↾ (V ×
V))𝑦)) |
| 33 | 32 | elv 3485 |
. . . . . . 7
⊢ (𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 〈𝐵, 𝐶〉(2nd ↾ (V ×
V))𝑦) |
| 34 | | brres 6004 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ V → (〈𝐵, 𝐶〉(2nd ↾ (V ×
V))𝑦 ↔ (〈𝐵, 𝐶〉 ∈ (V × V) ∧
〈𝐵, 𝐶〉2nd 𝑦))) |
| 35 | 34 | elv 3485 |
. . . . . . . . . 10
⊢
(〈𝐵, 𝐶〉(2nd ↾ (V
× V))𝑦 ↔
(〈𝐵, 𝐶〉 ∈ (V × V) ∧
〈𝐵, 𝐶〉2nd 𝑦)) |
| 36 | 15 | biantrurd 532 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉2nd 𝑦 ↔ (〈𝐵, 𝐶〉 ∈ (V × V) ∧
〈𝐵, 𝐶〉2nd 𝑦))) |
| 37 | 35, 36 | bitr4id 290 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉(2nd ↾ (V ×
V))𝑦 ↔ 〈𝐵, 𝐶〉2nd 𝑦)) |
| 38 | | br2ndeqg 8037 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉2nd 𝑦 ↔ 𝑦 = 𝐶)) |
| 39 | 37, 38 | bitrd 279 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉(2nd ↾ (V ×
V))𝑦 ↔ 𝑦 = 𝐶)) |
| 40 | 39 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐵, 𝐶〉(2nd ↾ (V ×
V))𝑦 ↔ 𝑦 = 𝐶)) |
| 41 | 33, 40 | bitrid 283 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉 ↔ 𝑦 = 𝐶)) |
| 42 | 41 | anbi1cd 635 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉) ↔ (𝑦 = 𝐶 ∧ 𝐴𝑆𝑦))) |
| 43 | 42 | exbidv 1921 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))〈𝐵, 𝐶〉) ↔ ∃𝑦(𝑦 = 𝐶 ∧ 𝐴𝑆𝑦))) |
| 44 | | breq2 5147 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝐴𝑆𝑦 ↔ 𝐴𝑆𝐶)) |
| 45 | 44 | ceqsexgv 3654 |
. . . . 5
⊢ (𝐶 ∈ 𝑋 → (∃𝑦(𝑦 = 𝐶 ∧ 𝐴𝑆𝑦) ↔ 𝐴𝑆𝐶)) |
| 46 | 45 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑦(𝑦 = 𝐶 ∧ 𝐴𝑆𝑦) ↔ 𝐴𝑆𝐶)) |
| 47 | 30, 43, 46 | 3bitrd 305 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)〈𝐵, 𝐶〉 ↔ 𝐴𝑆𝐶)) |
| 48 | 27, 47 | anbi12d 632 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴(◡(1st ↾ (V × V))
∘ 𝑅)〈𝐵, 𝐶〉 ∧ 𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)〈𝐵, 𝐶〉) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶))) |
| 49 | 3, 5, 48 | 3bitrd 305 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)〈𝐵, 𝐶〉 ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶))) |