Step | Hyp | Ref
| Expression |
1 | | efgval.w |
. . . . 5
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2𝑜)) |
2 | | efgval.r |
. . . . 5
⊢ ∼ = (
~FG ‘𝐼) |
3 | | efgval2.m |
. . . . 5
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2𝑜 ↦
〈𝑦,
(1𝑜 ∖ 𝑧)〉) |
4 | | efgval2.t |
. . . . 5
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(#‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦
(𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
5 | | efgred.d |
. . . . 5
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
6 | | efgred.s |
. . . . 5
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(#‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((#‘𝑚) − 1))) |
7 | 1, 2, 3, 4, 5, 6 | efgsfo 18152 |
. . . 4
⊢ 𝑆:dom 𝑆–onto→𝑊 |
8 | | foelrn 6378 |
. . . 4
⊢ ((𝑆:dom 𝑆–onto→𝑊 ∧ 𝐴 ∈ 𝑊) → ∃𝑎 ∈ dom 𝑆 𝐴 = (𝑆‘𝑎)) |
9 | 7, 8 | mpan 706 |
. . 3
⊢ (𝐴 ∈ 𝑊 → ∃𝑎 ∈ dom 𝑆 𝐴 = (𝑆‘𝑎)) |
10 | 1, 2, 3, 4, 5, 6 | efgsdm 18143 |
. . . . . . . 8
⊢ (𝑎 ∈ dom 𝑆 ↔ (𝑎 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑎‘0) ∈ 𝐷 ∧ ∀𝑖 ∈ (1..^(#‘𝑎))(𝑎‘𝑖) ∈ ran (𝑇‘(𝑎‘(𝑖 − 1))))) |
11 | 10 | simp2bi 1077 |
. . . . . . 7
⊢ (𝑎 ∈ dom 𝑆 → (𝑎‘0) ∈ 𝐷) |
12 | 11 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑎 ∈ dom 𝑆) → (𝑎‘0) ∈ 𝐷) |
13 | 1, 2, 3, 4, 5, 6 | efgsrel 18147 |
. . . . . . 7
⊢ (𝑎 ∈ dom 𝑆 → (𝑎‘0) ∼ (𝑆‘𝑎)) |
14 | 13 | adantl 482 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑎 ∈ dom 𝑆) → (𝑎‘0) ∼ (𝑆‘𝑎)) |
15 | | breq1 4656 |
. . . . . . 7
⊢ (𝑑 = (𝑎‘0) → (𝑑 ∼ (𝑆‘𝑎) ↔ (𝑎‘0) ∼ (𝑆‘𝑎))) |
16 | 15 | rspcev 3309 |
. . . . . 6
⊢ (((𝑎‘0) ∈ 𝐷 ∧ (𝑎‘0) ∼ (𝑆‘𝑎)) → ∃𝑑 ∈ 𝐷 𝑑 ∼ (𝑆‘𝑎)) |
17 | 12, 14, 16 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑎 ∈ dom 𝑆) → ∃𝑑 ∈ 𝐷 𝑑 ∼ (𝑆‘𝑎)) |
18 | | breq2 4657 |
. . . . . 6
⊢ (𝐴 = (𝑆‘𝑎) → (𝑑 ∼ 𝐴 ↔ 𝑑 ∼ (𝑆‘𝑎))) |
19 | 18 | rexbidv 3052 |
. . . . 5
⊢ (𝐴 = (𝑆‘𝑎) → (∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴 ↔ ∃𝑑 ∈ 𝐷 𝑑 ∼ (𝑆‘𝑎))) |
20 | 17, 19 | syl5ibrcom 237 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑎 ∈ dom 𝑆) → (𝐴 = (𝑆‘𝑎) → ∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴)) |
21 | 20 | rexlimdva 3031 |
. . 3
⊢ (𝐴 ∈ 𝑊 → (∃𝑎 ∈ dom 𝑆 𝐴 = (𝑆‘𝑎) → ∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴)) |
22 | 9, 21 | mpd 15 |
. 2
⊢ (𝐴 ∈ 𝑊 → ∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴) |
23 | 1, 2 | efger 18131 |
. . . . . . 7
⊢ ∼ Er
𝑊 |
24 | 23 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → ∼ Er 𝑊) |
25 | | simprl 794 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑑 ∼ 𝐴) |
26 | | simprr 796 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑐 ∼ 𝐴) |
27 | 24, 25, 26 | ertr4d 7761 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑑 ∼ 𝑐) |
28 | 1, 2, 3, 4, 5, 6 | efgrelex 18164 |
. . . . . 6
⊢ (𝑑 ∼ 𝑐 → ∃𝑎 ∈ (◡𝑆 “ {𝑑})∃𝑏 ∈ (◡𝑆 “ {𝑐})(𝑎‘0) = (𝑏‘0)) |
29 | | fofn 6117 |
. . . . . . . . . . . . . 14
⊢ (𝑆:dom 𝑆–onto→𝑊 → 𝑆 Fn dom 𝑆) |
30 | | fniniseg 6338 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Fn dom 𝑆 → (𝑎 ∈ (◡𝑆 “ {𝑑}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑑))) |
31 | 7, 29, 30 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (◡𝑆 “ {𝑑}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑑)) |
32 | 31 | simplbi 476 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (◡𝑆 “ {𝑑}) → 𝑎 ∈ dom 𝑆) |
33 | 32 | ad2antrl 764 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑎 ∈ dom 𝑆) |
34 | 1, 2, 3, 4, 5, 6 | efgsval 18144 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ dom 𝑆 → (𝑆‘𝑎) = (𝑎‘((#‘𝑎) − 1))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑎) = (𝑎‘((#‘𝑎) − 1))) |
36 | 31 | simprbi 480 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (◡𝑆 “ {𝑑}) → (𝑆‘𝑎) = 𝑑) |
37 | 36 | ad2antrl 764 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑎) = 𝑑) |
38 | | simpllr 799 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) |
39 | 38 | simpld 475 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑑 ∈ 𝐷) |
40 | 37, 39 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑎) ∈ 𝐷) |
41 | 1, 2, 3, 4, 5, 6 | efgs1b 18149 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ dom 𝑆 → ((𝑆‘𝑎) ∈ 𝐷 ↔ (#‘𝑎) = 1)) |
42 | 33, 41 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑆‘𝑎) ∈ 𝐷 ↔ (#‘𝑎) = 1)) |
43 | 40, 42 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (#‘𝑎) = 1) |
44 | 43 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((#‘𝑎) − 1) = (1 −
1)) |
45 | | 1m1e0 11089 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
46 | 44, 45 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((#‘𝑎) − 1) = 0) |
47 | 46 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑎‘((#‘𝑎) − 1)) = (𝑎‘0)) |
48 | 35, 37, 47 | 3eqtr3rd 2665 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑎‘0) = 𝑑) |
49 | | fniniseg 6338 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Fn dom 𝑆 → (𝑏 ∈ (◡𝑆 “ {𝑐}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑐))) |
50 | 7, 29, 49 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (◡𝑆 “ {𝑐}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑐)) |
51 | 50 | simplbi 476 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (◡𝑆 “ {𝑐}) → 𝑏 ∈ dom 𝑆) |
52 | 51 | ad2antll 765 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑏 ∈ dom 𝑆) |
53 | 1, 2, 3, 4, 5, 6 | efgsval 18144 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ dom 𝑆 → (𝑆‘𝑏) = (𝑏‘((#‘𝑏) − 1))) |
54 | 52, 53 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑏) = (𝑏‘((#‘𝑏) − 1))) |
55 | 50 | simprbi 480 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (◡𝑆 “ {𝑐}) → (𝑆‘𝑏) = 𝑐) |
56 | 55 | ad2antll 765 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑏) = 𝑐) |
57 | 38 | simprd 479 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑐 ∈ 𝐷) |
58 | 56, 57 | eqeltrd 2701 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑏) ∈ 𝐷) |
59 | 1, 2, 3, 4, 5, 6 | efgs1b 18149 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ dom 𝑆 → ((𝑆‘𝑏) ∈ 𝐷 ↔ (#‘𝑏) = 1)) |
60 | 52, 59 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑆‘𝑏) ∈ 𝐷 ↔ (#‘𝑏) = 1)) |
61 | 58, 60 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (#‘𝑏) = 1) |
62 | 61 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((#‘𝑏) − 1) = (1 −
1)) |
63 | 62, 45 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((#‘𝑏) − 1) = 0) |
64 | 63 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑏‘((#‘𝑏) − 1)) = (𝑏‘0)) |
65 | 54, 56, 64 | 3eqtr3rd 2665 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑏‘0) = 𝑐) |
66 | 48, 65 | eqeq12d 2637 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑎‘0) = (𝑏‘0) ↔ 𝑑 = 𝑐)) |
67 | 66 | biimpd 219 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑎‘0) = (𝑏‘0) → 𝑑 = 𝑐)) |
68 | 67 | rexlimdvva 3038 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → (∃𝑎 ∈ (◡𝑆 “ {𝑑})∃𝑏 ∈ (◡𝑆 “ {𝑐})(𝑎‘0) = (𝑏‘0) → 𝑑 = 𝑐)) |
69 | 28, 68 | syl5 34 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → (𝑑 ∼ 𝑐 → 𝑑 = 𝑐)) |
70 | 27, 69 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑑 = 𝑐) |
71 | 70 | ex 450 |
. . 3
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴) → 𝑑 = 𝑐)) |
72 | 71 | ralrimivva 2971 |
. 2
⊢ (𝐴 ∈ 𝑊 → ∀𝑑 ∈ 𝐷 ∀𝑐 ∈ 𝐷 ((𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴) → 𝑑 = 𝑐)) |
73 | | breq1 4656 |
. . 3
⊢ (𝑑 = 𝑐 → (𝑑 ∼ 𝐴 ↔ 𝑐 ∼ 𝐴)) |
74 | 73 | reu4 3400 |
. 2
⊢
(∃!𝑑 ∈
𝐷 𝑑 ∼ 𝐴 ↔ (∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴 ∧ ∀𝑑 ∈ 𝐷 ∀𝑐 ∈ 𝐷 ((𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴) → 𝑑 = 𝑐))) |
75 | 22, 72, 74 | sylanbrc 698 |
1
⊢ (𝐴 ∈ 𝑊 → ∃!𝑑 ∈ 𝐷 𝑑 ∼ 𝐴) |