Step | Hyp | Ref
| Expression |
1 | | eldif 3222 |
. . . 4
⊢ (⟨⟨x, y⟩, w⟩ ∈ (((A × B)
× V) ∖ (( Ins2 S ⊕ Ins3 R) “
1c)) ↔ (⟨⟨x, y⟩, w⟩ ∈ ((A ×
B) × V) ∧ ¬ ⟨⟨x, y⟩, w⟩ ∈ (( Ins2 S ⊕ Ins3 R) “ 1c))) |
2 | | vex 2863 |
. . . . . . 7
⊢ w ∈
V |
3 | | opelxp 4812 |
. . . . . . 7
⊢ (⟨⟨x, y⟩, w⟩ ∈ ((A × B)
× V) ↔ (⟨x, y⟩ ∈ (A × B)
∧ w ∈ V)) |
4 | 2, 3 | mpbiran2 885 |
. . . . . 6
⊢ (⟨⟨x, y⟩, w⟩ ∈ ((A × B)
× V) ↔ ⟨x, y⟩ ∈ (A × B)) |
5 | | opelxp 4812 |
. . . . . 6
⊢ (⟨x, y⟩ ∈ (A ×
B) ↔ (x ∈ A ∧ y ∈ B)) |
6 | 4, 5 | bitri 240 |
. . . . 5
⊢ (⟨⟨x, y⟩, w⟩ ∈ ((A × B)
× V) ↔ (x ∈ A ∧ y ∈ B)) |
7 | | dfcleq 2347 |
. . . . . 6
⊢ (w = V ↔
∀z(z ∈ w ↔
z ∈
V)) |
8 | | elima1c 4948 |
. . . . . . . 8
⊢ (⟨⟨x, y⟩, w⟩ ∈ (( Ins2 S ⊕ Ins3 R) “
1c) ↔ ∃z⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ ( Ins2 S ⊕ Ins3 R)) |
9 | | elsymdif 3224 |
. . . . . . . . . 10
⊢ (⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ ( Ins2 S ⊕ Ins3 R) ↔ ¬ (⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins2 S ↔ ⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins3 R)) |
10 | | vex 2863 |
. . . . . . . . . . . . . 14
⊢ x ∈
V |
11 | | vex 2863 |
. . . . . . . . . . . . . 14
⊢ y ∈
V |
12 | 10, 11 | opex 4589 |
. . . . . . . . . . . . 13
⊢ ⟨x, y⟩ ∈ V |
13 | 12 | otelins2 5792 |
. . . . . . . . . . . 12
⊢ (⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins2 S ↔ ⟨{z}, w⟩ ∈ S ) |
14 | | vex 2863 |
. . . . . . . . . . . . 13
⊢ z ∈
V |
15 | 14, 2 | opelssetsn 4761 |
. . . . . . . . . . . 12
⊢ (⟨{z}, w⟩ ∈ S ↔ z ∈ w) |
16 | 13, 15 | bitri 240 |
. . . . . . . . . . 11
⊢ (⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins2 S ↔ z ∈ w) |
17 | 2 | otelins3 5793 |
. . . . . . . . . . . 12
⊢ (⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins3 R ↔ ⟨{z}, ⟨x, y⟩⟩ ∈ R) |
18 | | releqmpt2.1 |
. . . . . . . . . . . 12
⊢ (⟨{z}, ⟨x, y⟩⟩ ∈ R ↔ z ∈ V) |
19 | 17, 18 | bitri 240 |
. . . . . . . . . . 11
⊢ (⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins3 R ↔ z ∈ V) |
20 | 16, 19 | bibi12i 306 |
. . . . . . . . . 10
⊢ ((⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins2 S ↔ ⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ Ins3 R) ↔
(z ∈
w ↔ z ∈ V)) |
21 | 9, 20 | xchbinx 301 |
. . . . . . . . 9
⊢ (⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ ( Ins2 S ⊕ Ins3 R) ↔ ¬ (z ∈ w ↔ z ∈ V)) |
22 | 21 | exbii 1582 |
. . . . . . . 8
⊢ (∃z⟨{z}, ⟨⟨x, y⟩, w⟩⟩ ∈ ( Ins2 S ⊕ Ins3 R) ↔ ∃z ¬
(z ∈
w ↔ z ∈ V)) |
23 | | exnal 1574 |
. . . . . . . 8
⊢ (∃z ¬
(z ∈
w ↔ z ∈ V) ↔ ¬ ∀z(z ∈ w ↔ z ∈ V)) |
24 | 8, 22, 23 | 3bitri 262 |
. . . . . . 7
⊢ (⟨⟨x, y⟩, w⟩ ∈ (( Ins2 S ⊕ Ins3 R) “
1c) ↔ ¬ ∀z(z ∈ w ↔ z ∈ V)) |
25 | 24 | con2bii 322 |
. . . . . 6
⊢ (∀z(z ∈ w ↔ z ∈ V) ↔
¬ ⟨⟨x, y⟩, w⟩ ∈ (( Ins2 S ⊕ Ins3 R) “ 1c)) |
26 | 7, 25 | bitr2i 241 |
. . . . 5
⊢ (¬ ⟨⟨x, y⟩, w⟩ ∈ (( Ins2 S ⊕ Ins3 R) “
1c) ↔ w = V) |
27 | 6, 26 | anbi12i 678 |
. . . 4
⊢ ((⟨⟨x, y⟩, w⟩ ∈ ((A × B)
× V) ∧ ¬ ⟨⟨x, y⟩, w⟩ ∈ (( Ins2 S ⊕ Ins3 R) “
1c)) ↔ ((x ∈ A ∧ y ∈ B) ∧ w = V)) |
28 | 1, 27 | bitri 240 |
. . 3
⊢ (⟨⟨x, y⟩, w⟩ ∈ (((A × B)
× V) ∖ (( Ins2 S ⊕ Ins3 R) “
1c)) ↔ ((x ∈ A ∧ y ∈ B) ∧ w = V)) |
29 | 28 | oprabbi2i 5648 |
. 2
⊢ (((A × B)
× V) ∖ (( Ins2 S ⊕ Ins3 R) “
1c)) = {⟨⟨x, y⟩, w⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ w = V)} |
30 | | df-mpt2 5655 |
. 2
⊢ (x ∈ A, y ∈ B ↦ V) = {⟨⟨x, y⟩, w⟩ ∣ ((x ∈ A ∧ y ∈ B) ∧ w = V)} |
31 | 29, 30 | eqtr4i 2376 |
1
⊢ (((A × B)
× V) ∖ (( Ins2 S ⊕ Ins3 R) “
1c)) = (x ∈ A, y ∈ B ↦ V) |