Step | Hyp | Ref
| Expression |
1 | | brcnv 4892 |
. . . . . 6
⊢ (z◡Wp ↔
pWz) |
2 | | brcnv 4892 |
. . . . . 6
⊢ (z◡Wq ↔
qWz) |
3 | | breldm 4911 |
. . . . . . . . 9
⊢ (pWz → p ∈ dom W) |
4 | | enprmaplem3.1 |
. . . . . . . . . . 11
⊢ W = (r ∈ (A
↑m B) ↦ (◡r
“ {x})) |
5 | 4 | enprmaplem2 6077 |
. . . . . . . . . 10
⊢ W Fn (A
↑m B) |
6 | | fndm 5182 |
. . . . . . . . . 10
⊢ (W Fn (A
↑m B) → dom
W = (A
↑m B)) |
7 | 5, 6 | ax-mp 5 |
. . . . . . . . 9
⊢ dom W = (A
↑m B) |
8 | 3, 7 | syl6eleq 2443 |
. . . . . . . 8
⊢ (pWz → p ∈ (A
↑m B)) |
9 | | fnfun 5181 |
. . . . . . . . . . 11
⊢ (W Fn (A
↑m B) → Fun
W) |
10 | 5, 9 | ax-mp 5 |
. . . . . . . . . 10
⊢ Fun W |
11 | | funbrfv 5356 |
. . . . . . . . . 10
⊢ (Fun W → (pWz → (W
‘p) = z)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . . . 9
⊢ (pWz → (W
‘p) = z) |
13 | | cnveq 4886 |
. . . . . . . . . . . 12
⊢ (r = p →
◡r
= ◡p) |
14 | 13 | imaeq1d 4941 |
. . . . . . . . . . 11
⊢ (r = p →
(◡r
“ {x}) = (◡p
“ {x})) |
15 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ p ∈
V |
16 | 15 | cnvex 5102 |
. . . . . . . . . . . 12
⊢ ◡p ∈ V |
17 | | snex 4111 |
. . . . . . . . . . . 12
⊢ {x} ∈
V |
18 | 16, 17 | imaex 4747 |
. . . . . . . . . . 11
⊢ (◡p
“ {x}) ∈ V |
19 | 14, 4, 18 | fvmpt 5700 |
. . . . . . . . . 10
⊢ (p ∈ (A ↑m B) → (W
‘p) = (◡p
“ {x})) |
20 | 8, 19 | syl 15 |
. . . . . . . . 9
⊢ (pWz → (W
‘p) = (◡p
“ {x})) |
21 | 12, 20 | eqtr3d 2387 |
. . . . . . . 8
⊢ (pWz → z =
(◡p
“ {x})) |
22 | 8, 21 | jca 518 |
. . . . . . 7
⊢ (pWz → (p
∈ (A
↑m B) ∧ z = (◡p
“ {x}))) |
23 | | breldm 4911 |
. . . . . . . . 9
⊢ (qWz → q ∈ dom W) |
24 | 23, 7 | syl6eleq 2443 |
. . . . . . . 8
⊢ (qWz → q ∈ (A
↑m B)) |
25 | | funbrfv 5356 |
. . . . . . . . . 10
⊢ (Fun W → (qWz → (W
‘q) = z)) |
26 | 10, 25 | ax-mp 5 |
. . . . . . . . 9
⊢ (qWz → (W
‘q) = z) |
27 | | cnveq 4886 |
. . . . . . . . . . . 12
⊢ (r = q →
◡r
= ◡q) |
28 | 27 | imaeq1d 4941 |
. . . . . . . . . . 11
⊢ (r = q →
(◡r
“ {x}) = (◡q
“ {x})) |
29 | | vex 2862 |
. . . . . . . . . . . . 13
⊢ q ∈
V |
30 | 29 | cnvex 5102 |
. . . . . . . . . . . 12
⊢ ◡q ∈ V |
31 | 30, 17 | imaex 4747 |
. . . . . . . . . . 11
⊢ (◡q
“ {x}) ∈ V |
32 | 28, 4, 31 | fvmpt 5700 |
. . . . . . . . . 10
⊢ (q ∈ (A ↑m B) → (W
‘q) = (◡q
“ {x})) |
33 | 24, 32 | syl 15 |
. . . . . . . . 9
⊢ (qWz → (W
‘q) = (◡q
“ {x})) |
34 | 26, 33 | eqtr3d 2387 |
. . . . . . . 8
⊢ (qWz → z =
(◡q
“ {x})) |
35 | 24, 34 | jca 518 |
. . . . . . 7
⊢ (qWz → (q
∈ (A
↑m B) ∧ z = (◡q
“ {x}))) |
36 | 22, 35 | anim12i 549 |
. . . . . 6
⊢ ((pWz ∧ qWz) → ((p
∈ (A
↑m B) ∧ z = (◡p
“ {x})) ∧ (q ∈ (A
↑m B) ∧ z = (◡q
“ {x})))) |
37 | 1, 2, 36 | syl2anb 465 |
. . . . 5
⊢ ((z◡Wp ∧ z◡Wq) →
((p ∈
(A ↑m B) ∧ z = (◡p
“ {x})) ∧ (q ∈ (A
↑m B) ∧ z = (◡q
“ {x})))) |
38 | | elmapi 6016 |
. . . . . . . . 9
⊢ (p ∈ (A ↑m B) → p:B–→A) |
39 | | elmapi 6016 |
. . . . . . . . 9
⊢ (q ∈ (A ↑m B) → q:B–→A) |
40 | 38, 39 | anim12i 549 |
. . . . . . . 8
⊢ ((p ∈ (A ↑m B) ∧ q ∈ (A ↑m B)) → (p:B–→A
∧ q:B–→A)) |
41 | | eqtr2 2371 |
. . . . . . . 8
⊢ ((z = (◡p
“ {x}) ∧ z = (◡q
“ {x})) → (◡p
“ {x}) = (◡q
“ {x})) |
42 | | simprll 738 |
. . . . . . . . . . 11
⊢ (((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) → p:B–→A) |
43 | | ffn 5223 |
. . . . . . . . . . 11
⊢ (p:B–→A
→ p Fn B) |
44 | 42, 43 | syl 15 |
. . . . . . . . . 10
⊢ (((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) → p Fn B) |
45 | | simprlr 739 |
. . . . . . . . . . 11
⊢ (((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) → q:B–→A) |
46 | | ffn 5223 |
. . . . . . . . . . 11
⊢ (q:B–→A
→ q Fn B) |
47 | 45, 46 | syl 15 |
. . . . . . . . . 10
⊢ (((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) → q Fn B) |
48 | | ffvelrn 5415 |
. . . . . . . . . . . 12
⊢ ((p:B–→A
∧ z ∈ B) →
(p ‘z) ∈ A) |
49 | 42, 48 | sylan 457 |
. . . . . . . . . . 11
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(p ‘z) ∈ A) |
50 | | simpllr 735 |
. . . . . . . . . . . . . 14
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
A = {x,
y}) |
51 | 50 | eleq2d 2420 |
. . . . . . . . . . . . 13
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) ∈ A ↔ (p
‘z) ∈ {x, y})) |
52 | | fvex 5339 |
. . . . . . . . . . . . . 14
⊢ (p ‘z)
∈ V |
53 | 52 | elpr 3751 |
. . . . . . . . . . . . 13
⊢ ((p ‘z)
∈ {x,
y} ↔ ((p ‘z) =
x ∨
(p ‘z) = y)) |
54 | 51, 53 | syl6bb 252 |
. . . . . . . . . . . 12
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) ∈ A ↔ ((p
‘z) = x ∨ (p ‘z) =
y))) |
55 | | simprr 733 |
. . . . . . . . . . . . . . 15
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ (p
‘z) = x)) → (p
‘z) = x) |
56 | | simplrr 737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(◡p
“ {x}) = (◡q
“ {x})) |
57 | 56 | eleq2d 2420 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(z ∈
(◡p
“ {x}) ↔ z ∈ (◡q
“ {x}))) |
58 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . 19
⊢ (z ∈ (◡p
“ {x}) ↔ zpx) |
59 | | eliniseg 5020 |
. . . . . . . . . . . . . . . . . . 19
⊢ (z ∈ (◡q
“ {x}) ↔ zqx) |
60 | 57, 58, 59 | 3bitr3g 278 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(zpx ↔
zqx)) |
61 | 60 | biimpd 198 |
. . . . . . . . . . . . . . . . 17
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(zpx →
zqx)) |
62 | | fnbrfvb 5358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((p Fn B ∧ z ∈ B) →
((p ‘z) = x ↔
zpx)) |
63 | 44, 62 | sylan 457 |
. . . . . . . . . . . . . . . . 17
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) = x ↔
zpx)) |
64 | | fnbrfvb 5358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((q Fn B ∧ z ∈ B) →
((q ‘z) = x ↔
zqx)) |
65 | 47, 64 | sylan 457 |
. . . . . . . . . . . . . . . . 17
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((q ‘z) = x ↔
zqx)) |
66 | 61, 63, 65 | 3imtr4d 259 |
. . . . . . . . . . . . . . . 16
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) = x →
(q ‘z) = x)) |
67 | 66 | impr 602 |
. . . . . . . . . . . . . . 15
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ (p
‘z) = x)) → (q
‘z) = x) |
68 | 55, 67 | eqtr4d 2388 |
. . . . . . . . . . . . . 14
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ (p
‘z) = x)) → (p
‘z) = (q ‘z)) |
69 | 68 | expr 598 |
. . . . . . . . . . . . 13
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) = x →
(p ‘z) = (q
‘z))) |
70 | | simprr 733 |
. . . . . . . . . . . . . . 15
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ (p
‘z) = y)) → (p
‘z) = y) |
71 | | simplll 734 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
x ≠ y) |
72 | 71 | neneqd 2532 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
¬ x = y) |
73 | 42 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
p:B–→A) |
74 | | ffun 5225 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (p:B–→A
→ Fun p) |
75 | | fununiq 5517 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Fun p ∧ zpx ∧ zpy) → x =
y) |
76 | 75 | 3expib 1154 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Fun p → ((zpx ∧ zpy) → x =
y)) |
77 | 76 | ancomsd 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Fun p → ((zpy ∧ zpx) → x =
y)) |
78 | 73, 74, 77 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((zpy ∧ zpx) →
x = y)) |
79 | 78 | exp3a 425 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(zpy →
(zpx →
x = y))) |
80 | 79 | impr 602 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(zpx →
x = y)) |
81 | 72, 80 | mtod 168 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
¬ zpx) |
82 | 81 | expr 598 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(zpy → ¬
zpx)) |
83 | 60 | biimprd 214 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(zqx →
zpx)) |
84 | 82, 83 | nsyld 132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(zpy → ¬
zqx)) |
85 | 84 | impr 602 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
¬ zqx) |
86 | | simprl 732 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
z ∈
B) |
87 | 45 | adantr 451 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
q:B–→A) |
88 | | fdm 5226 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (q:B–→A
→ dom q = B) |
89 | 87, 88 | syl 15 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) → dom
q = B) |
90 | 86, 89 | eleqtrrd 2430 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
z ∈ dom
q) |
91 | | eldm 4898 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (z ∈ dom q ↔ ∃w zqw) |
92 | | brelrn 4960 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (zqw → w ∈ ran q) |
93 | | frn 5228 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (q:B–→A
→ ran q ⊆ A) |
94 | 87, 93 | syl 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) → ran
q ⊆
A) |
95 | 94 | sseld 3272 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(w ∈ ran
q → w ∈ A)) |
96 | 92, 95 | syl5 28 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(zqw →
w ∈
A)) |
97 | | simpllr 735 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
A = {x,
y}) |
98 | 97 | eleq2d 2420 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(w ∈
A ↔ w ∈ {x, y})) |
99 | | vex 2862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ w ∈
V |
100 | 99 | elpr 3751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (w ∈ {x, y} ↔
(w = x
∨ w =
y)) |
101 | | breq2 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (w = x →
(zqw ↔
zqx)) |
102 | 101 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (zqw → (w =
x → zqx)) |
103 | | breq2 4643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (w = y →
(zqw ↔
zqy)) |
104 | 103 | biimpcd 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (zqw → (w =
y → zqy)) |
105 | 102, 104 | orim12d 811 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (zqw → ((w =
x ∨
w = y)
→ (zqx ∨ zqy))) |
106 | 105 | com12 27 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((w = x ∨ w = y) → (zqw → (zqx ∨ zqy))) |
107 | 100, 106 | sylbi 187 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (w ∈ {x, y} →
(zqw →
(zqx ∨ zqy))) |
108 | 98, 107 | syl6bi 219 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(w ∈
A → (zqw → (zqx ∨ zqy)))) |
109 | 108 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(zqw →
(w ∈
A → (zqx ∨ zqy)))) |
110 | 96, 109 | mpdd 36 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(zqw →
(zqx ∨ zqy))) |
111 | 110 | exlimdv 1636 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(∃w
zqw →
(zqx ∨ zqy))) |
112 | 91, 111 | syl5bi 208 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(z ∈ dom
q → (zqx ∨ zqy))) |
113 | 90, 112 | mpd 14 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
(zqx ∨ zqy)) |
114 | | orel1 371 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬ zqx → ((zqx ∨ zqy) → zqy)) |
115 | 85, 113, 114 | sylc 56 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ zpy)) →
zqy) |
116 | 115 | expr 598 |
. . . . . . . . . . . . . . . . 17
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(zpy →
zqy)) |
117 | | fnbrfvb 5358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((p Fn B ∧ z ∈ B) →
((p ‘z) = y ↔
zpy)) |
118 | 44, 117 | sylan 457 |
. . . . . . . . . . . . . . . . 17
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) = y ↔
zpy)) |
119 | | fnbrfvb 5358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((q Fn B ∧ z ∈ B) →
((q ‘z) = y ↔
zqy)) |
120 | 47, 119 | sylan 457 |
. . . . . . . . . . . . . . . . 17
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((q ‘z) = y ↔
zqy)) |
121 | 116, 118,
120 | 3imtr4d 259 |
. . . . . . . . . . . . . . . 16
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) = y →
(q ‘z) = y)) |
122 | 121 | impr 602 |
. . . . . . . . . . . . . . 15
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ (p
‘z) = y)) → (q
‘z) = y) |
123 | 70, 122 | eqtr4d 2388 |
. . . . . . . . . . . . . 14
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ (z ∈ B ∧ (p
‘z) = y)) → (p
‘z) = (q ‘z)) |
124 | 123 | expr 598 |
. . . . . . . . . . . . 13
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) = y →
(p ‘z) = (q
‘z))) |
125 | 69, 124 | jaod 369 |
. . . . . . . . . . . 12
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(((p ‘z) = x ∨ (p
‘z) = y) → (p
‘z) = (q ‘z))) |
126 | 54, 125 | sylbid 206 |
. . . . . . . . . . 11
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
((p ‘z) ∈ A → (p
‘z) = (q ‘z))) |
127 | 49, 126 | mpd 14 |
. . . . . . . . . 10
⊢ ((((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) ∧ z ∈ B) →
(p ‘z) = (q
‘z)) |
128 | 44, 47, 127 | eqfnfvd 5395 |
. . . . . . . . 9
⊢ (((x ≠ y ∧ A = {x, y}) ∧ ((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x}))) → p = q) |
129 | 128 | expcom 424 |
. . . . . . . 8
⊢ (((p:B–→A
∧ q:B–→A)
∧ (◡p
“ {x}) = (◡q
“ {x})) → ((x ≠ y ∧ A = {x, y}) →
p = q)) |
130 | 40, 41, 129 | syl2an 463 |
. . . . . . 7
⊢ (((p ∈ (A ↑m B) ∧ q ∈ (A ↑m B)) ∧ (z = (◡p
“ {x}) ∧ z = (◡q
“ {x}))) → ((x ≠ y ∧ A = {x, y}) →
p = q)) |
131 | 130 | an4s 799 |
. . . . . 6
⊢ (((p ∈ (A ↑m B) ∧ z = (◡p
“ {x})) ∧ (q ∈ (A
↑m B) ∧ z = (◡q
“ {x}))) → ((x ≠ y ∧ A = {x, y}) →
p = q)) |
132 | 131 | com12 27 |
. . . . 5
⊢ ((x ≠ y ∧ A = {x, y}) →
(((p ∈
(A ↑m B) ∧ z = (◡p
“ {x})) ∧ (q ∈ (A
↑m B) ∧ z = (◡q
“ {x}))) → p = q)) |
133 | 37, 132 | syl5 28 |
. . . 4
⊢ ((x ≠ y ∧ A = {x, y}) →
((z◡Wp ∧ z◡Wq) →
p = q)) |
134 | 133 | alrimiv 1631 |
. . 3
⊢ ((x ≠ y ∧ A = {x, y}) →
∀q((z◡Wp ∧ z◡Wq) →
p = q)) |
135 | 134 | alrimivv 1632 |
. 2
⊢ ((x ≠ y ∧ A = {x, y}) →
∀z∀p∀q((z◡Wp ∧ z◡Wq) →
p = q)) |
136 | | dffun2 5119 |
. 2
⊢ (Fun ◡W ↔
∀z∀p∀q((z◡Wp ∧ z◡Wq) →
p = q)) |
137 | 135, 136 | sylibr 203 |
1
⊢ ((x ≠ y ∧ A = {x, y}) →
Fun ◡W) |