Step | Hyp | Ref
| Expression |
1 | | vdgr1.1 |
. . 3
⊢ (𝜑 → 𝑉 ∈ V) |
2 | | vdgr1.2 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
3 | | snex 4835 |
. . . . 5
⊢ {𝑈} ∈ V |
4 | | f1osng 6089 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ {𝑈} ∈ V) → {〈𝐴, {𝑈}〉}:{𝐴}–1-1-onto→{{𝑈}}) |
5 | 2, 3, 4 | sylancl 693 |
. . . 4
⊢ (𝜑 → {〈𝐴, {𝑈}〉}:{𝐴}–1-1-onto→{{𝑈}}) |
6 | | f1ofn 6051 |
. . . 4
⊢
({〈𝐴, {𝑈}〉}:{𝐴}–1-1-onto→{{𝑈}} → {〈𝐴, {𝑈}〉} Fn {𝐴}) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → {〈𝐴, {𝑈}〉} Fn {𝐴}) |
8 | | snex 4835 |
. . . 4
⊢ {𝐴} ∈ V |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → {𝐴} ∈ V) |
10 | | vdgr1.3 |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
11 | | vdgrval 26423 |
. . 3
⊢ (((𝑉 ∈ V ∧ {〈𝐴, {𝑈}〉} Fn {𝐴} ∧ {𝐴} ∈ V) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg {〈𝐴, {𝑈}〉})‘𝑈) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}))) |
12 | 1, 7, 9, 10, 11 | syl31anc 1321 |
. 2
⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝑈}〉})‘𝑈) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}))) |
13 | | hashrabrsn 13022 |
. . . 4
⊢
(#‘{𝑥 ∈
{𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) ∈
ℕ0 |
14 | 13 | nn0rei 11180 |
. . 3
⊢
(#‘{𝑥 ∈
{𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) ∈ ℝ |
15 | | hashrabrsn 13022 |
. . . . 5
⊢
(#‘{𝑥 ∈
{𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}) ∈
ℕ0 |
16 | 15 | nn0rei 11180 |
. . . 4
⊢
(#‘{𝑥 ∈
{𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}) ∈ ℝ |
17 | 16 | a1i 11 |
. . 3
⊢ (𝜑 → (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}) ∈ ℝ) |
18 | | rexadd 11937 |
. . 3
⊢
(((#‘{𝑥 ∈
{𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) ∈ ℝ ∧ (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}) ∈ ℝ) → ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}))) |
19 | 14, 17, 18 | sylancr 694 |
. 2
⊢ (𝜑 → ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}))) |
20 | | snidg 4153 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ {𝑈}) |
21 | 10, 20 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ {𝑈}) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐴}) → 𝑈 ∈ {𝑈}) |
23 | | elsni 4142 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝐴} → 𝑥 = 𝐴) |
24 | 23 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑥 ∈ {𝐴} → ({〈𝐴, {𝑈}〉}‘𝑥) = ({〈𝐴, {𝑈}〉}‘𝐴)) |
25 | | fvsng 6352 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ V ∧ {𝑈} ∈ V) → ({〈𝐴, {𝑈}〉}‘𝐴) = {𝑈}) |
26 | 2, 3, 25 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝜑 → ({〈𝐴, {𝑈}〉}‘𝐴) = {𝑈}) |
27 | 24, 26 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐴}) → ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}) |
28 | 22, 27 | eleqtrrd 2691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐴}) → 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)) |
29 | 28 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ {𝐴}𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)) |
30 | | rabid2 3096 |
. . . . . . 7
⊢ ({𝐴} = {𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)} ↔ ∀𝑥 ∈ {𝐴}𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)) |
31 | 29, 30 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → {𝐴} = {𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) |
32 | 31 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘{𝐴}) = (#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)})) |
33 | | hashsng 13020 |
. . . . . 6
⊢ (𝐴 ∈ V → (#‘{𝐴}) = 1) |
34 | 2, 33 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝐴}) = 1) |
35 | 32, 34 | eqtr3d 2646 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) = 1) |
36 | 27 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ {𝐴} ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}) |
37 | | rabid2 3096 |
. . . . . . 7
⊢ ({𝐴} = {𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}} ↔ ∀𝑥 ∈ {𝐴} ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}) |
38 | 36, 37 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → {𝐴} = {𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}) |
39 | 38 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘{𝐴}) = (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}})) |
40 | 39, 34 | eqtr3d 2646 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}}) = 1) |
41 | 35, 40 | oveq12d 6567 |
. . 3
⊢ (𝜑 → ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}})) = (1 + 1)) |
42 | | df-2 10956 |
. . 3
⊢ 2 = (1 +
1) |
43 | 41, 42 | syl6eqr 2662 |
. 2
⊢ (𝜑 → ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈}〉}‘𝑥) = {𝑈}})) = 2) |
44 | 12, 19, 43 | 3eqtrd 2648 |
1
⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝑈}〉})‘𝑈) = 2) |