| Step | Hyp | Ref
| Expression |
| 1 | | efgval.w |
. . . . 5
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) |
| 2 | | efgval.r |
. . . . 5
⊢ ∼ = (
~FG ‘𝐼) |
| 3 | | efgval2.m |
. . . . 5
⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) |
| 4 | | efgval2.t |
. . . . 5
⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) |
| 5 | | efgred.d |
. . . . 5
⊢ 𝐷 = (𝑊 ∖ ∪
𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) |
| 6 | | efgred.s |
. . . . 5
⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈
(1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) |
| 7 | 1, 2, 3, 4, 5, 6 | efgsfo 19757 |
. . . 4
⊢ 𝑆:dom 𝑆–onto→𝑊 |
| 8 | | foelrn 7127 |
. . . 4
⊢ ((𝑆:dom 𝑆–onto→𝑊 ∧ 𝐴 ∈ 𝑊) → ∃𝑎 ∈ dom 𝑆 𝐴 = (𝑆‘𝑎)) |
| 9 | 7, 8 | mpan 690 |
. . 3
⊢ (𝐴 ∈ 𝑊 → ∃𝑎 ∈ dom 𝑆 𝐴 = (𝑆‘𝑎)) |
| 10 | 1, 2, 3, 4, 5, 6 | efgsdm 19748 |
. . . . . . 7
⊢ (𝑎 ∈ dom 𝑆 ↔ (𝑎 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝑎‘0) ∈ 𝐷 ∧ ∀𝑖 ∈
(1..^(♯‘𝑎))(𝑎‘𝑖) ∈ ran (𝑇‘(𝑎‘(𝑖 − 1))))) |
| 11 | 10 | simp2bi 1147 |
. . . . . 6
⊢ (𝑎 ∈ dom 𝑆 → (𝑎‘0) ∈ 𝐷) |
| 12 | 1, 2, 3, 4, 5, 6 | efgsrel 19752 |
. . . . . . 7
⊢ (𝑎 ∈ dom 𝑆 → (𝑎‘0) ∼ (𝑆‘𝑎)) |
| 13 | 12 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑎 ∈ dom 𝑆) → (𝑎‘0) ∼ (𝑆‘𝑎)) |
| 14 | | breq1 5146 |
. . . . . . 7
⊢ (𝑑 = (𝑎‘0) → (𝑑 ∼ (𝑆‘𝑎) ↔ (𝑎‘0) ∼ (𝑆‘𝑎))) |
| 15 | 14 | rspcev 3622 |
. . . . . 6
⊢ (((𝑎‘0) ∈ 𝐷 ∧ (𝑎‘0) ∼ (𝑆‘𝑎)) → ∃𝑑 ∈ 𝐷 𝑑 ∼ (𝑆‘𝑎)) |
| 16 | 11, 13, 15 | syl2an2 686 |
. . . . 5
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑎 ∈ dom 𝑆) → ∃𝑑 ∈ 𝐷 𝑑 ∼ (𝑆‘𝑎)) |
| 17 | | breq2 5147 |
. . . . . 6
⊢ (𝐴 = (𝑆‘𝑎) → (𝑑 ∼ 𝐴 ↔ 𝑑 ∼ (𝑆‘𝑎))) |
| 18 | 17 | rexbidv 3179 |
. . . . 5
⊢ (𝐴 = (𝑆‘𝑎) → (∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴 ↔ ∃𝑑 ∈ 𝐷 𝑑 ∼ (𝑆‘𝑎))) |
| 19 | 16, 18 | syl5ibrcom 247 |
. . . 4
⊢ ((𝐴 ∈ 𝑊 ∧ 𝑎 ∈ dom 𝑆) → (𝐴 = (𝑆‘𝑎) → ∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴)) |
| 20 | 19 | rexlimdva 3155 |
. . 3
⊢ (𝐴 ∈ 𝑊 → (∃𝑎 ∈ dom 𝑆 𝐴 = (𝑆‘𝑎) → ∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴)) |
| 21 | 9, 20 | mpd 15 |
. 2
⊢ (𝐴 ∈ 𝑊 → ∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴) |
| 22 | 1, 2 | efger 19736 |
. . . . . . 7
⊢ ∼ Er
𝑊 |
| 23 | 22 | a1i 11 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → ∼ Er 𝑊) |
| 24 | | simprl 771 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑑 ∼ 𝐴) |
| 25 | | simprr 773 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑐 ∼ 𝐴) |
| 26 | 23, 24, 25 | ertr4d 8764 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑑 ∼ 𝑐) |
| 27 | 1, 2, 3, 4, 5, 6 | efgrelex 19769 |
. . . . . 6
⊢ (𝑑 ∼ 𝑐 → ∃𝑎 ∈ (◡𝑆 “ {𝑑})∃𝑏 ∈ (◡𝑆 “ {𝑐})(𝑎‘0) = (𝑏‘0)) |
| 28 | | fofn 6822 |
. . . . . . . . . . . . . 14
⊢ (𝑆:dom 𝑆–onto→𝑊 → 𝑆 Fn dom 𝑆) |
| 29 | | fniniseg 7080 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Fn dom 𝑆 → (𝑎 ∈ (◡𝑆 “ {𝑑}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑑))) |
| 30 | 7, 28, 29 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (◡𝑆 “ {𝑑}) ↔ (𝑎 ∈ dom 𝑆 ∧ (𝑆‘𝑎) = 𝑑)) |
| 31 | 30 | simplbi 497 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (◡𝑆 “ {𝑑}) → 𝑎 ∈ dom 𝑆) |
| 32 | 31 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑎 ∈ dom 𝑆) |
| 33 | 1, 2, 3, 4, 5, 6 | efgsval 19749 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ dom 𝑆 → (𝑆‘𝑎) = (𝑎‘((♯‘𝑎) − 1))) |
| 34 | 32, 33 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑎) = (𝑎‘((♯‘𝑎) − 1))) |
| 35 | 30 | simprbi 496 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (◡𝑆 “ {𝑑}) → (𝑆‘𝑎) = 𝑑) |
| 36 | 35 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑎) = 𝑑) |
| 37 | | simpllr 776 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) |
| 38 | 37 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑑 ∈ 𝐷) |
| 39 | 36, 38 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑎) ∈ 𝐷) |
| 40 | 1, 2, 3, 4, 5, 6 | efgs1b 19754 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ dom 𝑆 → ((𝑆‘𝑎) ∈ 𝐷 ↔ (♯‘𝑎) = 1)) |
| 41 | 32, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑆‘𝑎) ∈ 𝐷 ↔ (♯‘𝑎) = 1)) |
| 42 | 39, 41 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (♯‘𝑎) = 1) |
| 43 | 42 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((♯‘𝑎) − 1) = (1 −
1)) |
| 44 | | 1m1e0 12338 |
. . . . . . . . . . . 12
⊢ (1
− 1) = 0 |
| 45 | 43, 44 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((♯‘𝑎) − 1) =
0) |
| 46 | 45 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑎‘((♯‘𝑎) − 1)) = (𝑎‘0)) |
| 47 | 34, 36, 46 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑎‘0) = 𝑑) |
| 48 | | fniniseg 7080 |
. . . . . . . . . . . . . 14
⊢ (𝑆 Fn dom 𝑆 → (𝑏 ∈ (◡𝑆 “ {𝑐}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑐))) |
| 49 | 7, 28, 48 | mp2b 10 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ (◡𝑆 “ {𝑐}) ↔ (𝑏 ∈ dom 𝑆 ∧ (𝑆‘𝑏) = 𝑐)) |
| 50 | 49 | simplbi 497 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ (◡𝑆 “ {𝑐}) → 𝑏 ∈ dom 𝑆) |
| 51 | 50 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑏 ∈ dom 𝑆) |
| 52 | 1, 2, 3, 4, 5, 6 | efgsval 19749 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ dom 𝑆 → (𝑆‘𝑏) = (𝑏‘((♯‘𝑏) − 1))) |
| 53 | 51, 52 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑏) = (𝑏‘((♯‘𝑏) − 1))) |
| 54 | 49 | simprbi 496 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ (◡𝑆 “ {𝑐}) → (𝑆‘𝑏) = 𝑐) |
| 55 | 54 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑏) = 𝑐) |
| 56 | 37 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → 𝑐 ∈ 𝐷) |
| 57 | 55, 56 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑆‘𝑏) ∈ 𝐷) |
| 58 | 1, 2, 3, 4, 5, 6 | efgs1b 19754 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 ∈ dom 𝑆 → ((𝑆‘𝑏) ∈ 𝐷 ↔ (♯‘𝑏) = 1)) |
| 59 | 51, 58 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑆‘𝑏) ∈ 𝐷 ↔ (♯‘𝑏) = 1)) |
| 60 | 57, 59 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (♯‘𝑏) = 1) |
| 61 | 60 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((♯‘𝑏) − 1) = (1 −
1)) |
| 62 | 61, 44 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((♯‘𝑏) − 1) =
0) |
| 63 | 62 | fveq2d 6910 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑏‘((♯‘𝑏) − 1)) = (𝑏‘0)) |
| 64 | 53, 55, 63 | 3eqtr3rd 2786 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → (𝑏‘0) = 𝑐) |
| 65 | 47, 64 | eqeq12d 2753 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑎‘0) = (𝑏‘0) ↔ 𝑑 = 𝑐)) |
| 66 | 65 | biimpd 229 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) ∧ (𝑎 ∈ (◡𝑆 “ {𝑑}) ∧ 𝑏 ∈ (◡𝑆 “ {𝑐}))) → ((𝑎‘0) = (𝑏‘0) → 𝑑 = 𝑐)) |
| 67 | 66 | rexlimdvva 3213 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → (∃𝑎 ∈ (◡𝑆 “ {𝑑})∃𝑏 ∈ (◡𝑆 “ {𝑐})(𝑎‘0) = (𝑏‘0) → 𝑑 = 𝑐)) |
| 68 | 27, 67 | syl5 34 |
. . . . 5
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → (𝑑 ∼ 𝑐 → 𝑑 = 𝑐)) |
| 69 | 26, 68 | mpd 15 |
. . . 4
⊢ (((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) ∧ (𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴)) → 𝑑 = 𝑐) |
| 70 | 69 | ex 412 |
. . 3
⊢ ((𝐴 ∈ 𝑊 ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴) → 𝑑 = 𝑐)) |
| 71 | 70 | ralrimivva 3202 |
. 2
⊢ (𝐴 ∈ 𝑊 → ∀𝑑 ∈ 𝐷 ∀𝑐 ∈ 𝐷 ((𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴) → 𝑑 = 𝑐)) |
| 72 | | breq1 5146 |
. . 3
⊢ (𝑑 = 𝑐 → (𝑑 ∼ 𝐴 ↔ 𝑐 ∼ 𝐴)) |
| 73 | 72 | reu4 3737 |
. 2
⊢
(∃!𝑑 ∈
𝐷 𝑑 ∼ 𝐴 ↔ (∃𝑑 ∈ 𝐷 𝑑 ∼ 𝐴 ∧ ∀𝑑 ∈ 𝐷 ∀𝑐 ∈ 𝐷 ((𝑑 ∼ 𝐴 ∧ 𝑐 ∼ 𝐴) → 𝑑 = 𝑐))) |
| 74 | 21, 71, 73 | sylanbrc 583 |
1
⊢ (𝐴 ∈ 𝑊 → ∃!𝑑 ∈ 𝐷 𝑑 ∼ 𝐴) |