Step | Hyp | Ref
| Expression |
1 | | difss 3064 |
. . . . 5
⊢ (𝐹 ∖ 𝐺) ⊆ 𝐹 |
2 | | dmss 4477 |
. . . . 5
⊢ ((𝐹 ∖ 𝐺) ⊆ 𝐹 → dom (𝐹 ∖ 𝐺) ⊆ dom 𝐹) |
3 | 1, 2 | ax-mp 7 |
. . . 4
⊢ dom
(𝐹 ∖ 𝐺) ⊆ dom 𝐹 |
4 | | fndm 4941 |
. . . . 5
⊢ (𝐹 Fn A → dom 𝐹 = A) |
5 | 4 | adantr 261 |
. . . 4
⊢ ((𝐹 Fn A ∧ 𝐺 Fn A) → dom 𝐹 = A) |
6 | 3, 5 | syl5sseq 2987 |
. . 3
⊢ ((𝐹 Fn A ∧ 𝐺 Fn A) → dom (𝐹 ∖ 𝐺) ⊆ A) |
7 | | dfss1 3135 |
. . 3
⊢ (dom
(𝐹 ∖ 𝐺) ⊆ A ↔ (A
∩ dom (𝐹 ∖ 𝐺)) = dom (𝐹 ∖ 𝐺)) |
8 | 6, 7 | sylib 127 |
. 2
⊢ ((𝐹 Fn A ∧ 𝐺 Fn A) → (A
∩ dom (𝐹 ∖ 𝐺)) = dom (𝐹 ∖ 𝐺)) |
9 | | vex 2554 |
. . . . 5
⊢ x ∈
V |
10 | 9 | eldm 4475 |
. . . 4
⊢ (x ∈ dom (𝐹 ∖ 𝐺) ↔ ∃y x(𝐹 ∖ 𝐺)y) |
11 | | eqcom 2039 |
. . . . . . . 8
⊢ ((𝐹‘x) = (𝐺‘x) ↔ (𝐺‘x) = (𝐹‘x)) |
12 | | fnbrfvb 5157 |
. . . . . . . 8
⊢ ((𝐺 Fn A ∧ x ∈ A) → ((𝐺‘x) = (𝐹‘x) ↔ x𝐺(𝐹‘x))) |
13 | 11, 12 | syl5bb 181 |
. . . . . . 7
⊢ ((𝐺 Fn A ∧ x ∈ A) → ((𝐹‘x) = (𝐺‘x) ↔ x𝐺(𝐹‘x))) |
14 | 13 | adantll 445 |
. . . . . 6
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → ((𝐹‘x) = (𝐺‘x) ↔ x𝐺(𝐹‘x))) |
15 | 14 | necon3abid 2238 |
. . . . 5
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → ((𝐹‘x) ≠ (𝐺‘x) ↔ ¬ x𝐺(𝐹‘x))) |
16 | | funfvex 5135 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ x ∈ dom 𝐹) → (𝐹‘x) ∈
V) |
17 | 16 | funfni 4942 |
. . . . . . 7
⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹‘x) ∈
V) |
18 | 17 | adantlr 446 |
. . . . . 6
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → (𝐹‘x) ∈
V) |
19 | | breq2 3759 |
. . . . . . . 8
⊢ (y = (𝐹‘x) → (x𝐺y ↔
x𝐺(𝐹‘x))) |
20 | 19 | notbid 591 |
. . . . . . 7
⊢ (y = (𝐹‘x) → (¬ x𝐺y ↔
¬ x𝐺(𝐹‘x))) |
21 | 20 | ceqsexgv 2667 |
. . . . . 6
⊢ ((𝐹‘x) ∈ V →
(∃y(y = (𝐹‘x) ∧ ¬ x𝐺y)
↔ ¬ x𝐺(𝐹‘x))) |
22 | 18, 21 | syl 14 |
. . . . 5
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → (∃y(y = (𝐹‘x) ∧ ¬ x𝐺y)
↔ ¬ x𝐺(𝐹‘x))) |
23 | | eqcom 2039 |
. . . . . . . . . 10
⊢ (y = (𝐹‘x) ↔ (𝐹‘x) = y) |
24 | | fnbrfvb 5157 |
. . . . . . . . . 10
⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹‘x) = y ↔
x𝐹y)) |
25 | 23, 24 | syl5bb 181 |
. . . . . . . . 9
⊢ ((𝐹 Fn A ∧ x ∈ A) → (y =
(𝐹‘x) ↔ x𝐹y)) |
26 | 25 | adantlr 446 |
. . . . . . . 8
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → (y =
(𝐹‘x) ↔ x𝐹y)) |
27 | 26 | anbi1d 438 |
. . . . . . 7
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → ((y =
(𝐹‘x) ∧ ¬ x𝐺y)
↔ (x𝐹y ∧ ¬ x𝐺y))) |
28 | | brdif 3803 |
. . . . . . 7
⊢ (x(𝐹 ∖ 𝐺)y
↔ (x𝐹y ∧ ¬ x𝐺y)) |
29 | 27, 28 | syl6bbr 187 |
. . . . . 6
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → ((y =
(𝐹‘x) ∧ ¬ x𝐺y)
↔ x(𝐹 ∖ 𝐺)y)) |
30 | 29 | exbidv 1703 |
. . . . 5
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → (∃y(y = (𝐹‘x) ∧ ¬ x𝐺y)
↔ ∃y x(𝐹 ∖ 𝐺)y)) |
31 | 15, 22, 30 | 3bitr2rd 206 |
. . . 4
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → (∃y x(𝐹 ∖ 𝐺)y
↔ (𝐹‘x) ≠ (𝐺‘x))) |
32 | 10, 31 | syl5bb 181 |
. . 3
⊢ (((𝐹 Fn A ∧ 𝐺 Fn A) ∧ x ∈ A) → (x
∈ dom (𝐹 ∖ 𝐺) ↔ (𝐹‘x) ≠ (𝐺‘x))) |
33 | 32 | rabbi2dva 3139 |
. 2
⊢ ((𝐹 Fn A ∧ 𝐺 Fn A) → (A
∩ dom (𝐹 ∖ 𝐺)) = {x ∈ A ∣ (𝐹‘x) ≠ (𝐺‘x)}) |
34 | 8, 33 | eqtr3d 2071 |
1
⊢ ((𝐹 Fn A ∧ 𝐺 Fn A) → dom (𝐹 ∖ 𝐺) = {x
∈ A
∣ (𝐹‘x) ≠ (𝐺‘x)}) |