Step | Hyp | Ref
| Expression |
1 | | df-xrn 37236 |
. . . 4
⊢ (𝑅 ⋉ 𝑆) = ((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆)) |
2 | 1 | breqi 5154 |
. . 3
⊢ (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ 𝐴((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆))⟨𝐵, 𝐶⟩) |
3 | 2 | a1i 11 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ 𝐴((◡(1st ↾ (V × V))
∘ 𝑅) ∩ (◡(2nd ↾ (V × V))
∘ 𝑆))⟨𝐵, 𝐶⟩)) |
4 | | brin 5200 |
. . 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 5464 |
. . . . . 6
⊢
⟨𝐵, 𝐶⟩ ∈ V |
7 | | brcog 5866 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ⟨𝐵, 𝐶⟩ ∈ V) → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)⟨𝐵, 𝐶⟩ ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩))) |
8 | 6, 7 | mpan2 689 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)⟨𝐵, 𝐶⟩ ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩))) |
9 | 8 | 3ad2ant1 1133 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)⟨𝐵, 𝐶⟩ ↔ ∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩))) |
10 | | brcnvg 5879 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ ⟨𝐵, 𝐶⟩ ∈ V) → (𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩(1st ↾ (V ×
V))𝑥)) |
11 | 6, 10 | mpan2 689 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩(1st ↾ (V ×
V))𝑥)) |
12 | 11 | elv 3480 |
. . . . . . 7
⊢ (𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩(1st ↾ (V ×
V))𝑥) |
13 | | brres 5988 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ V → (⟨𝐵, 𝐶⟩(1st ↾ (V ×
V))𝑥 ↔ (⟨𝐵, 𝐶⟩ ∈ (V × V) ∧
⟨𝐵, 𝐶⟩1st 𝑥))) |
14 | 13 | elv 3480 |
. . . . . . . . . 10
⊢
(⟨𝐵, 𝐶⟩(1st ↾ (V
× V))𝑥 ↔
(⟨𝐵, 𝐶⟩ ∈ (V × V) ∧
⟨𝐵, 𝐶⟩1st 𝑥)) |
15 | | opelvvg 5717 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ⟨𝐵, 𝐶⟩ ∈ (V ×
V)) |
16 | 15 | biantrurd 533 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩1st 𝑥 ↔ (⟨𝐵, 𝐶⟩ ∈ (V × V) ∧
⟨𝐵, 𝐶⟩1st 𝑥))) |
17 | 14, 16 | bitr4id 289 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩(1st ↾ (V ×
V))𝑥 ↔ ⟨𝐵, 𝐶⟩1st 𝑥)) |
18 | | br1steqg 7996 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩1st 𝑥 ↔ 𝑥 = 𝐵)) |
19 | 17, 18 | bitrd 278 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩(1st ↾ (V ×
V))𝑥 ↔ 𝑥 = 𝐵)) |
20 | 19 | 3adant1 1130 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩(1st ↾ (V ×
V))𝑥 ↔ 𝑥 = 𝐵)) |
21 | 12, 20 | bitrid 282 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ 𝑥 = 𝐵)) |
22 | 21 | anbi1cd 634 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩) ↔ (𝑥 = 𝐵 ∧ 𝐴𝑅𝑥))) |
23 | 22 | exbidv 1924 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥(𝐴𝑅𝑥 ∧ 𝑥◡(1st ↾ (V ×
V))⟨𝐵, 𝐶⟩) ↔ ∃𝑥(𝑥 = 𝐵 ∧ 𝐴𝑅𝑥))) |
24 | | breq2 5152 |
. . . . . 6
⊢ (𝑥 = 𝐵 → (𝐴𝑅𝑥 ↔ 𝐴𝑅𝐵)) |
25 | 24 | ceqsexgv 3642 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → (∃𝑥(𝑥 = 𝐵 ∧ 𝐴𝑅𝑥) ↔ 𝐴𝑅𝐵)) |
26 | 25 | 3ad2ant2 1134 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑥(𝑥 = 𝐵 ∧ 𝐴𝑅𝑥) ↔ 𝐴𝑅𝐵)) |
27 | 9, 23, 26 | 3bitrd 304 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(1st ↾ (V × V))
∘ 𝑅)⟨𝐵, 𝐶⟩ ↔ 𝐴𝑅𝐵)) |
28 | | brcog 5866 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ ⟨𝐵, 𝐶⟩ ∈ V) → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)⟨𝐵, 𝐶⟩ ↔ ∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩))) |
29 | 6, 28 | mpan2 689 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)⟨𝐵, 𝐶⟩ ↔ ∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩))) |
30 | 29 | 3ad2ant1 1133 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)⟨𝐵, 𝐶⟩ ↔ ∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩))) |
31 | | brcnvg 5879 |
. . . . . . . . 9
⊢ ((𝑦 ∈ V ∧ ⟨𝐵, 𝐶⟩ ∈ V) → (𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩(2nd ↾ (V ×
V))𝑦)) |
32 | 6, 31 | mpan2 689 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩(2nd ↾ (V ×
V))𝑦)) |
33 | 32 | elv 3480 |
. . . . . . 7
⊢ (𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ ⟨𝐵, 𝐶⟩(2nd ↾ (V ×
V))𝑦) |
34 | | brres 5988 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ V → (⟨𝐵, 𝐶⟩(2nd ↾ (V ×
V))𝑦 ↔ (⟨𝐵, 𝐶⟩ ∈ (V × V) ∧
⟨𝐵, 𝐶⟩2nd 𝑦))) |
35 | 34 | elv 3480 |
. . . . . . . . . 10
⊢
(⟨𝐵, 𝐶⟩(2nd ↾ (V
× V))𝑦 ↔
(⟨𝐵, 𝐶⟩ ∈ (V × V) ∧
⟨𝐵, 𝐶⟩2nd 𝑦)) |
36 | 15 | biantrurd 533 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩2nd 𝑦 ↔ (⟨𝐵, 𝐶⟩ ∈ (V × V) ∧
⟨𝐵, 𝐶⟩2nd 𝑦))) |
37 | 35, 36 | bitr4id 289 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩(2nd ↾ (V ×
V))𝑦 ↔ ⟨𝐵, 𝐶⟩2nd 𝑦)) |
38 | | br2ndeqg 7997 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩2nd 𝑦 ↔ 𝑦 = 𝐶)) |
39 | 37, 38 | bitrd 278 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩(2nd ↾ (V ×
V))𝑦 ↔ 𝑦 = 𝐶)) |
40 | 39 | 3adant1 1130 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (⟨𝐵, 𝐶⟩(2nd ↾ (V ×
V))𝑦 ↔ 𝑦 = 𝐶)) |
41 | 33, 40 | bitrid 282 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩ ↔ 𝑦 = 𝐶)) |
42 | 41 | anbi1cd 634 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩) ↔ (𝑦 = 𝐶 ∧ 𝐴𝑆𝑦))) |
43 | 42 | exbidv 1924 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑦(𝐴𝑆𝑦 ∧ 𝑦◡(2nd ↾ (V ×
V))⟨𝐵, 𝐶⟩) ↔ ∃𝑦(𝑦 = 𝐶 ∧ 𝐴𝑆𝑦))) |
44 | | breq2 5152 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝐴𝑆𝑦 ↔ 𝐴𝑆𝐶)) |
45 | 44 | ceqsexgv 3642 |
. . . . 5
⊢ (𝐶 ∈ 𝑋 → (∃𝑦(𝑦 = 𝐶 ∧ 𝐴𝑆𝑦) ↔ 𝐴𝑆𝐶)) |
46 | 45 | 3ad2ant3 1135 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (∃𝑦(𝑦 = 𝐶 ∧ 𝐴𝑆𝑦) ↔ 𝐴𝑆𝐶)) |
47 | 30, 43, 46 | 3bitrd 304 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)⟨𝐵, 𝐶⟩ ↔ 𝐴𝑆𝐶)) |
48 | 27, 47 | anbi12d 631 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → ((𝐴(◡(1st ↾ (V × V))
∘ 𝑅)⟨𝐵, 𝐶⟩ ∧ 𝐴(◡(2nd ↾ (V × V))
∘ 𝑆)⟨𝐵, 𝐶⟩) ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶))) |
49 | 3, 5, 48 | 3bitrd 304 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (𝐴(𝑅 ⋉ 𝑆)⟨𝐵, 𝐶⟩ ↔ (𝐴𝑅𝐵 ∧ 𝐴𝑆𝐶))) |