Step | Hyp | Ref
| Expression |
1 | | vdgr1.1 |
. . . 4
⊢ (𝜑 → 𝑉 ∈ V) |
2 | | vdgr1.2 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ V) |
3 | | prex 4836 |
. . . . . 6
⊢ {𝑈, 𝐵} ∈ V |
4 | | f1osng 6089 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ {𝑈, 𝐵} ∈ V) → {〈𝐴, {𝑈, 𝐵}〉}:{𝐴}–1-1-onto→{{𝑈, 𝐵}}) |
5 | 2, 3, 4 | sylancl 693 |
. . . . 5
⊢ (𝜑 → {〈𝐴, {𝑈, 𝐵}〉}:{𝐴}–1-1-onto→{{𝑈, 𝐵}}) |
6 | | f1ofn 6051 |
. . . . 5
⊢
({〈𝐴, {𝑈, 𝐵}〉}:{𝐴}–1-1-onto→{{𝑈, 𝐵}} → {〈𝐴, {𝑈, 𝐵}〉} Fn {𝐴}) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → {〈𝐴, {𝑈, 𝐵}〉} Fn {𝐴}) |
8 | | snex 4835 |
. . . . 5
⊢ {𝐴} ∈ V |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝜑 → {𝐴} ∈ V) |
10 | | vdgr1.3 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
11 | | vdgrval 26423 |
. . . 4
⊢ (((𝑉 ∈ V ∧ {〈𝐴, {𝑈, 𝐵}〉} Fn {𝐴} ∧ {𝐴} ∈ V) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg {〈𝐴, {𝑈, 𝐵}〉})‘𝑈) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}))) |
12 | 1, 7, 9, 10, 11 | syl31anc 1321 |
. . 3
⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝑈, 𝐵}〉})‘𝑈) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}))) |
13 | | hashrabrsn 13022 |
. . . . 5
⊢
(#‘{𝑥 ∈
{𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) ∈
ℕ0 |
14 | 13 | nn0rei 11180 |
. . . 4
⊢
(#‘{𝑥 ∈
{𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) ∈ ℝ |
15 | | hashrabrsn 13022 |
. . . . 5
⊢
(#‘{𝑥 ∈
{𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}) ∈
ℕ0 |
16 | 15 | nn0rei 11180 |
. . . 4
⊢
(#‘{𝑥 ∈
{𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}) ∈ ℝ |
17 | | rexadd 11937 |
. . . 4
⊢
(((#‘{𝑥 ∈
{𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) ∈ ℝ ∧ (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}) ∈ ℝ) → ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}))) |
18 | 14, 16, 17 | mp2an 704 |
. . 3
⊢
((#‘{𝑥 ∈
{𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) +𝑒 (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}})) |
19 | 12, 18 | syl6eq 2660 |
. 2
⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝑈, 𝐵}〉})‘𝑈) = ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}))) |
20 | | prid1g 4239 |
. . . . . . . . . . 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 | | vdgr1.4 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
37 | | prid2g 4240 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝑈, 𝐵}) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ {𝑈, 𝐵}) |
39 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐴}) → 𝐵 ∈ {𝑈, 𝐵}) |
40 | 39, 27 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐴}) → 𝐵 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)) |
41 | | vdgr1.5 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ≠ 𝑈) |
42 | | nelsn 4159 |
. . . . . . . . . . 11
⊢ (𝐵 ≠ 𝑈 → ¬ 𝐵 ∈ {𝑈}) |
43 | 41, 42 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ¬ 𝐵 ∈ {𝑈}) |
44 | 43 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐴}) → ¬ 𝐵 ∈ {𝑈}) |
45 | | nelneq2 2713 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) ∧ ¬ 𝐵 ∈ {𝑈}) → ¬ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}) |
46 | 40, 44, 45 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ {𝐴}) → ¬ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}) |
47 | 46 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ {𝐴} ¬ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}) |
48 | | rabeq0 3911 |
. . . . . . 7
⊢ ({𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}} = ∅ ↔ ∀𝑥 ∈ {𝐴} ¬ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}) |
49 | 47, 48 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}} = ∅) |
50 | 49 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}) = (#‘∅)) |
51 | | hash0 13019 |
. . . . 5
⊢
(#‘∅) = 0 |
52 | 50, 51 | syl6eq 2660 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}}) = 0) |
53 | 35, 52 | oveq12d 6567 |
. . 3
⊢ (𝜑 → ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}})) = (1 + 0)) |
54 | | 1p0e1 11010 |
. . 3
⊢ (1 + 0) =
1 |
55 | 53, 54 | syl6eq 2660 |
. 2
⊢ (𝜑 → ((#‘{𝑥 ∈ {𝐴} ∣ 𝑈 ∈ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥)}) + (#‘{𝑥 ∈ {𝐴} ∣ ({〈𝐴, {𝑈, 𝐵}〉}‘𝑥) = {𝑈}})) = 1) |
56 | 19, 55 | eqtrd 2644 |
1
⊢ (𝜑 → ((𝑉 VDeg {〈𝐴, {𝑈, 𝐵}〉})‘𝑈) = 1) |