Step | Hyp | Ref
| Expression |
1 | | funiun 6412 |
. . 3
⊢ (Fun
𝐹 → 𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉}) |
2 | | eqeq1 2626 |
. . . . . . . . . 10
⊢ (𝐹 = 〈𝑋, 𝑌〉 → (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} ↔ 〈𝑋, 𝑌〉 = ∪
𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉})) |
3 | | eqcom 2629 |
. . . . . . . . . 10
⊢
(〈𝑋, 𝑌〉 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} ↔ ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = 〈𝑋, 𝑌〉) |
4 | 2, 3 | syl6bb 276 |
. . . . . . . . 9
⊢ (𝐹 = 〈𝑋, 𝑌〉 → (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} ↔ ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = 〈𝑋, 𝑌〉)) |
5 | 4 | adantl 482 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} ↔ ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = 〈𝑋, 𝑌〉)) |
6 | | funopsn.x |
. . . . . . . . . . 11
⊢ 𝑋 ∈ V |
7 | | funopsn.y |
. . . . . . . . . . 11
⊢ 𝑌 ∈ V |
8 | 6, 7 | opnzi 4943 |
. . . . . . . . . 10
⊢
〈𝑋, 𝑌〉 ≠
∅ |
9 | | neeq1 2856 |
. . . . . . . . . . . . . 14
⊢
(〈𝑋, 𝑌〉 = 𝐹 → (〈𝑋, 𝑌〉 ≠ ∅ ↔ 𝐹 ≠ ∅)) |
10 | 9 | eqcoms 2630 |
. . . . . . . . . . . . 13
⊢ (𝐹 = 〈𝑋, 𝑌〉 → (〈𝑋, 𝑌〉 ≠ ∅ ↔ 𝐹 ≠ ∅)) |
11 | | funrel 5905 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
𝐹 → Rel 𝐹) |
12 | | reldm0 5343 |
. . . . . . . . . . . . . . . . 17
⊢ (Rel
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝐹 → (𝐹 = ∅ ↔ dom 𝐹 = ∅)) |
14 | 13 | biimprd 238 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝐹 → (dom 𝐹 = ∅ → 𝐹 = ∅)) |
15 | 14 | necon3d 2815 |
. . . . . . . . . . . . . 14
⊢ (Fun
𝐹 → (𝐹 ≠ ∅ → dom 𝐹 ≠ ∅)) |
16 | 15 | com12 32 |
. . . . . . . . . . . . 13
⊢ (𝐹 ≠ ∅ → (Fun 𝐹 → dom 𝐹 ≠ ∅)) |
17 | 10, 16 | syl6bi 243 |
. . . . . . . . . . . 12
⊢ (𝐹 = 〈𝑋, 𝑌〉 → (〈𝑋, 𝑌〉 ≠ ∅ → (Fun 𝐹 → dom 𝐹 ≠ ∅))) |
18 | 17 | com3l 89 |
. . . . . . . . . . 11
⊢
(〈𝑋, 𝑌〉 ≠ ∅ → (Fun
𝐹 → (𝐹 = 〈𝑋, 𝑌〉 → dom 𝐹 ≠ ∅))) |
19 | 18 | impd 447 |
. . . . . . . . . 10
⊢
(〈𝑋, 𝑌〉 ≠ ∅ → ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → dom 𝐹 ≠ ∅)) |
20 | 8, 19 | ax-mp 5 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → dom 𝐹 ≠ ∅) |
21 | | fvex 6201 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) ∈ V |
22 | 21, 6, 7 | iunopeqop 4981 |
. . . . . . . . 9
⊢ (dom
𝐹 ≠ ∅ →
(∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = 〈𝑋, 𝑌〉 → ∃𝑎dom 𝐹 = {𝑎})) |
23 | 20, 22 | syl 17 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → (∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = 〈𝑋, 𝑌〉 → ∃𝑎dom 𝐹 = {𝑎})) |
24 | 5, 23 | sylbid 230 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} → ∃𝑎dom 𝐹 = {𝑎})) |
25 | 24 | imp 445 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉}) → ∃𝑎dom 𝐹 = {𝑎}) |
26 | | iuneq1 4534 |
. . . . . . . . . . . 12
⊢ (dom
𝐹 = {𝑎} → ∪
𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = ∪ 𝑥 ∈ {𝑎} {〈𝑥, (𝐹‘𝑥)〉}) |
27 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
28 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → 𝑥 = 𝑎) |
29 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
30 | 28, 29 | opeq12d 4410 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝑎, (𝐹‘𝑎)〉) |
31 | 30 | sneqd 4189 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → {〈𝑥, (𝐹‘𝑥)〉} = {〈𝑎, (𝐹‘𝑎)〉}) |
32 | 27, 31 | iunxsn 4603 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ {𝑎} {〈𝑥, (𝐹‘𝑥)〉} = {〈𝑎, (𝐹‘𝑎)〉} |
33 | 26, 32 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (dom
𝐹 = {𝑎} → ∪
𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = {〈𝑎, (𝐹‘𝑎)〉}) |
34 | 33 | adantl 482 |
. . . . . . . . . 10
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ dom 𝐹 = {𝑎}) → ∪
𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} = {〈𝑎, (𝐹‘𝑎)〉}) |
35 | 34 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ dom 𝐹 = {𝑎}) → (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} ↔ 𝐹 = {〈𝑎, (𝐹‘𝑎)〉})) |
36 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
⊢ (𝐹 = 〈𝑋, 𝑌〉 → (𝐹 = {〈𝑎, (𝐹‘𝑎)〉} ↔ 〈𝑋, 𝑌〉 = {〈𝑎, (𝐹‘𝑎)〉})) |
37 | 36 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → (𝐹 = {〈𝑎, (𝐹‘𝑎)〉} ↔ 〈𝑋, 𝑌〉 = {〈𝑎, (𝐹‘𝑎)〉})) |
38 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢
(〈𝑋, 𝑌〉 = {〈𝑎, (𝐹‘𝑎)〉} ↔ {〈𝑎, (𝐹‘𝑎)〉} = 〈𝑋, 𝑌〉) |
39 | | fvex 6201 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘𝑎) ∈ V |
40 | 27, 39, 6, 7 | snopeqop 4969 |
. . . . . . . . . . . . . 14
⊢
({〈𝑎, (𝐹‘𝑎)〉} = 〈𝑋, 𝑌〉 ↔ (𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎})) |
41 | 38, 40 | sylbb 209 |
. . . . . . . . . . . . 13
⊢
(〈𝑋, 𝑌〉 = {〈𝑎, (𝐹‘𝑎)〉} → (𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎})) |
42 | 37, 41 | syl6bi 243 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → (𝐹 = {〈𝑎, (𝐹‘𝑎)〉} → (𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}))) |
43 | 42 | imp 445 |
. . . . . . . . . . 11
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = {〈𝑎, (𝐹‘𝑎)〉}) → (𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎})) |
44 | | simpr3 1069 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 = {〈𝑎, (𝐹‘𝑎)〉} ∧ (𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎})) → 𝑋 = {𝑎}) |
45 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → 𝑎 = (𝐹‘𝑎)) |
46 | 45 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → (𝐹‘𝑎) = 𝑎) |
47 | 46 | opeq2d 4409 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → 〈𝑎, (𝐹‘𝑎)〉 = 〈𝑎, 𝑎〉) |
48 | 47 | sneqd 4189 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → {〈𝑎, (𝐹‘𝑎)〉} = {〈𝑎, 𝑎〉}) |
49 | 48 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → (𝐹 = {〈𝑎, (𝐹‘𝑎)〉} ↔ 𝐹 = {〈𝑎, 𝑎〉})) |
50 | 49 | biimpac 503 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 = {〈𝑎, (𝐹‘𝑎)〉} ∧ (𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎})) → 𝐹 = {〈𝑎, 𝑎〉}) |
51 | 44, 50 | jca 554 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 = {〈𝑎, (𝐹‘𝑎)〉} ∧ (𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎})) → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉})) |
52 | 51 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝐹 = {〈𝑎, (𝐹‘𝑎)〉} → ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
53 | 52 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = {〈𝑎, (𝐹‘𝑎)〉}) → ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
54 | 53 | a1dd 50 |
. . . . . . . . . . 11
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = {〈𝑎, (𝐹‘𝑎)〉}) → ((𝑎 = (𝐹‘𝑎) ∧ 𝑋 = 𝑌 ∧ 𝑋 = {𝑎}) → (dom 𝐹 = {𝑎} → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉})))) |
55 | 43, 54 | mpd 15 |
. . . . . . . . . 10
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = {〈𝑎, (𝐹‘𝑎)〉}) → (dom 𝐹 = {𝑎} → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
56 | 55 | impancom 456 |
. . . . . . . . 9
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ dom 𝐹 = {𝑎}) → (𝐹 = {〈𝑎, (𝐹‘𝑎)〉} → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
57 | 35, 56 | sylbid 230 |
. . . . . . . 8
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ dom 𝐹 = {𝑎}) → (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
58 | 57 | impancom 456 |
. . . . . . 7
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉}) → (dom 𝐹 = {𝑎} → (𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
59 | 58 | eximdv 1846 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉}) → (∃𝑎dom 𝐹 = {𝑎} → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
60 | 25, 59 | mpd 15 |
. . . . 5
⊢ (((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) ∧ 𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉}) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉})) |
61 | 60 | expcom 451 |
. . . 4
⊢ (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} → ((Fun 𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
62 | 61 | expd 452 |
. . 3
⊢ (𝐹 = ∪ 𝑥 ∈ dom 𝐹{〈𝑥, (𝐹‘𝑥)〉} → (Fun 𝐹 → (𝐹 = 〈𝑋, 𝑌〉 → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉})))) |
63 | 1, 62 | mpcom 38 |
. 2
⊢ (Fun
𝐹 → (𝐹 = 〈𝑋, 𝑌〉 → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉}))) |
64 | 63 | imp 445 |
1
⊢ ((Fun
𝐹 ∧ 𝐹 = 〈𝑋, 𝑌〉) → ∃𝑎(𝑋 = {𝑎} ∧ 𝐹 = {〈𝑎, 𝑎〉})) |