Step | Hyp | Ref
| Expression |
1 | | elun 3715 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
2 | 1 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))) |
3 | | andir 908 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)) ∨ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)))) |
4 | 2, 3 | bitri 263 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)) ∨ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)))) |
5 | 4 | abbii 2726 |
. . . . . . . 8
⊢ {𝑥 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)) ∨ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)))} |
6 | | df-rab 2905 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} |
7 | | unab 3853 |
. . . . . . . 8
⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)) ∨ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)))} |
8 | 5, 6, 7 | 3eqtr4i 2642 |
. . . . . . 7
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))}) |
9 | | df-rab 2905 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} |
10 | | vdgrun.e |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐸 Fn 𝐴) |
11 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐸 Fn 𝐴) |
12 | | vdgrun.f |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn 𝐵) |
13 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 Fn 𝐵) |
14 | | vdgrun.i |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) |
15 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ∩ 𝐵) = ∅) |
16 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
17 | | fvun1 6179 |
. . . . . . . . . . . 12
⊢ ((𝐸 Fn 𝐴 ∧ 𝐹 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑥 ∈ 𝐴)) → ((𝐸 ∪ 𝐹)‘𝑥) = (𝐸‘𝑥)) |
18 | 11, 13, 15, 16, 17 | syl112anc 1322 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐸 ∪ 𝐹)‘𝑥) = (𝐸‘𝑥)) |
19 | 18 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥) ↔ 𝑈 ∈ (𝐸‘𝑥))) |
20 | 19 | rabbidva 3163 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)} = {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) |
21 | 9, 20 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} = {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) |
22 | | df-rab 2905 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} |
23 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐸 Fn 𝐴) |
24 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝐹 Fn 𝐵) |
25 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝐴 ∩ 𝐵) = ∅) |
26 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
27 | | fvun2 6180 |
. . . . . . . . . . . 12
⊢ ((𝐸 Fn 𝐴 ∧ 𝐹 Fn 𝐵 ∧ ((𝐴 ∩ 𝐵) = ∅ ∧ 𝑥 ∈ 𝐵)) → ((𝐸 ∪ 𝐹)‘𝑥) = (𝐹‘𝑥)) |
28 | 23, 24, 25, 26, 27 | syl112anc 1322 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝐸 ∪ 𝐹)‘𝑥) = (𝐹‘𝑥)) |
29 | 28 | eleq2d 2673 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥) ↔ 𝑈 ∈ (𝐹‘𝑥))) |
30 | 29 | rabbidva 3163 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)} = {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) |
31 | 22, 30 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} = {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) |
32 | 21, 31 | uneq12d 3730 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))} ∪ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥))}) = ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∪ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)})) |
33 | 8, 32 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)} = ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∪ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)})) |
34 | 33 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)}) = (#‘({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∪ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}))) |
35 | | vdgrun.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑋) |
36 | | rabexg 4739 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
37 | 35, 36 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
38 | | vdgrun.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑌) |
39 | | rabexg 4739 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑌 → {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)} ∈ V) |
40 | 38, 39 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)} ∈ V) |
41 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ⊆ 𝐴 |
42 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)} ⊆ 𝐵 |
43 | | ss2in 3802 |
. . . . . . . . 9
⊢ (({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)} ⊆ 𝐵) → ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∩ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ⊆ (𝐴 ∩ 𝐵)) |
44 | 41, 42, 43 | mp2an 704 |
. . . . . . . 8
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∩ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ⊆ (𝐴 ∩ 𝐵) |
45 | 44, 14 | syl5sseq 3616 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∩ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ⊆ ∅) |
46 | | ss0 3926 |
. . . . . . 7
⊢ (({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∩ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ⊆ ∅ → ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∩ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) = ∅) |
47 | 45, 46 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∩ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) = ∅) |
48 | | hashunx 13036 |
. . . . . 6
⊢ (({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V ∧ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)} ∈ V ∧ ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∩ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) = ∅) → (#‘({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∪ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)})) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}))) |
49 | 37, 40, 47, 48 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (#‘({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∪ {𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)})) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}))) |
50 | 34, 49 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)}) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}))) |
51 | 1 | anbi1i 727 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})) |
52 | | andir 908 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}) ↔ ((𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}) ∨ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}))) |
53 | 51, 52 | bitri 263 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}) ↔ ((𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}) ∨ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}))) |
54 | 53 | abbii 2726 |
. . . . . . . 8
⊢ {𝑥 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}) ∨ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}))} |
55 | | df-rab 2905 |
. . . . . . . 8
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}} = {𝑥 ∣ (𝑥 ∈ (𝐴 ∪ 𝐵) ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} |
56 | | unab 3853 |
. . . . . . . 8
⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} ∪ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}) ∨ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}))} |
57 | 54, 55, 56 | 3eqtr4i 2642 |
. . . . . . 7
⊢ {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} ∪ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})}) |
58 | | df-rab 2905 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐴 ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} |
59 | 18 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝐸 ∪ 𝐹)‘𝑥) = {𝑈} ↔ (𝐸‘𝑥) = {𝑈})) |
60 | 59 | rabbidva 3163 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}} = {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) |
61 | 58, 60 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} = {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) |
62 | | df-rab 2905 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐵 ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} |
63 | 28 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝐸 ∪ 𝐹)‘𝑥) = {𝑈} ↔ (𝐹‘𝑥) = {𝑈})) |
64 | 63 | rabbidva 3163 |
. . . . . . . . 9
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}} = {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) |
65 | 62, 64 | syl5eqr 2658 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} = {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) |
66 | 61, 65 | uneq12d 3730 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})} ∪ {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈})}) = ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∪ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})) |
67 | 57, 66 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}} = ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∪ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})) |
68 | 67 | fveq2d 6107 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}}) = (#‘({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∪ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}))) |
69 | | rabexg 4739 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑋 → {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∈ V) |
70 | 35, 69 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∈ V) |
71 | | rabexg 4739 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑌 → {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}} ∈ V) |
72 | 38, 71 | syl 17 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}} ∈ V) |
73 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ⊆ 𝐴 |
74 | | ssrab2 3650 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}} ⊆ 𝐵 |
75 | | ss2in 3802 |
. . . . . . . . 9
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ⊆ 𝐴 ∧ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}} ⊆ 𝐵) → ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∩ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ⊆ (𝐴 ∩ 𝐵)) |
76 | 73, 74, 75 | mp2an 704 |
. . . . . . . 8
⊢ ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∩ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ⊆ (𝐴 ∩ 𝐵) |
77 | 76, 14 | syl5sseq 3616 |
. . . . . . 7
⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∩ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ⊆ ∅) |
78 | | ss0 3926 |
. . . . . . 7
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∩ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ⊆ ∅ → ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∩ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) = ∅) |
79 | 77, 78 | syl 17 |
. . . . . 6
⊢ (𝜑 → ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∩ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) = ∅) |
80 | | hashunx 13036 |
. . . . . 6
⊢ (({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∈ V ∧ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}} ∈ V ∧ ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∩ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) = ∅) → (#‘({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∪ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}))) |
81 | 70, 72, 79, 80 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (#‘({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∪ {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}))) |
82 | 68, 81 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}}) = ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}))) |
83 | 50, 82 | oveq12d 6567 |
. . 3
⊢ (𝜑 → ((#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}})) = (((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)})) +𝑒 ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})))) |
84 | | hashxrcl 13010 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V → (#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ∈
ℝ*) |
85 | 37, 84 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ∈
ℝ*) |
86 | | hashnemnf 12994 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V → (#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ≠ -∞) |
87 | 37, 86 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ≠ -∞) |
88 | 85, 87 | jca 553 |
. . . 4
⊢ (𝜑 → ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ∈ ℝ* ∧
(#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ≠ -∞)) |
89 | | hashxrcl 13010 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)} ∈ V → (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ∈
ℝ*) |
90 | 40, 89 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ∈
ℝ*) |
91 | | hashnemnf 12994 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)} ∈ V → (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ≠ -∞) |
92 | 40, 91 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ≠ -∞) |
93 | 90, 92 | jca 553 |
. . . 4
⊢ (𝜑 → ((#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ∈ ℝ* ∧
(#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) ≠ -∞)) |
94 | | hashxrcl 13010 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∈ V → (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) ∈
ℝ*) |
95 | 70, 94 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) ∈
ℝ*) |
96 | | hashnemnf 12994 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}} ∈ V → (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) ≠ -∞) |
97 | 70, 96 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) ≠ -∞) |
98 | 95, 97 | jca 553 |
. . . 4
⊢ (𝜑 → ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) ∈ ℝ* ∧
(#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) ≠ -∞)) |
99 | | hashxrcl 13010 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}} ∈ V → (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ∈
ℝ*) |
100 | 72, 99 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ∈
ℝ*) |
101 | | hashnemnf 12994 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}} ∈ V → (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ≠ -∞) |
102 | 72, 101 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ≠ -∞) |
103 | 100, 102 | jca 553 |
. . . 4
⊢ (𝜑 → ((#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ∈ ℝ* ∧
(#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}) ≠ -∞)) |
104 | 88, 93, 98, 103 | xadd4d 12005 |
. . 3
⊢ (𝜑 → (((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)})) +𝑒 ((#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}))) = (((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}})) +𝑒 ((#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})))) |
105 | 83, 104 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}})) = (((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}})) +𝑒 ((#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})))) |
106 | | relumgra 25843 |
. . . 4
⊢ Rel
UMGrph |
107 | | vdgrun.ge |
. . . 4
⊢ (𝜑 → 𝑉 UMGrph 𝐸) |
108 | | brrelex 5080 |
. . . 4
⊢ ((Rel
UMGrph ∧ 𝑉 UMGrph 𝐸) → 𝑉 ∈ V) |
109 | 106, 107,
108 | sylancr 694 |
. . 3
⊢ (𝜑 → 𝑉 ∈ V) |
110 | | fnun 5911 |
. . . 4
⊢ (((𝐸 Fn 𝐴 ∧ 𝐹 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐸 ∪ 𝐹) Fn (𝐴 ∪ 𝐵)) |
111 | 10, 12, 14, 110 | syl21anc 1317 |
. . 3
⊢ (𝜑 → (𝐸 ∪ 𝐹) Fn (𝐴 ∪ 𝐵)) |
112 | | unexg 6857 |
. . . 4
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴 ∪ 𝐵) ∈ V) |
113 | 35, 38, 112 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐴 ∪ 𝐵) ∈ V) |
114 | | vdgrun.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
115 | | vdgrval 26423 |
. . 3
⊢ (((𝑉 ∈ V ∧ (𝐸 ∪ 𝐹) Fn (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) ∈ V) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg (𝐸 ∪ 𝐹))‘𝑈) = ((#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}}))) |
116 | 109, 111,
113, 114, 115 | syl31anc 1321 |
. 2
⊢ (𝜑 → ((𝑉 VDeg (𝐸 ∪ 𝐹))‘𝑈) = ((#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ 𝑈 ∈ ((𝐸 ∪ 𝐹)‘𝑥)}) +𝑒 (#‘{𝑥 ∈ (𝐴 ∪ 𝐵) ∣ ((𝐸 ∪ 𝐹)‘𝑥) = {𝑈}}))) |
117 | | vdgrval 26423 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐸 Fn 𝐴 ∧ 𝐴 ∈ 𝑋) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}))) |
118 | 109, 10, 35, 114, 117 | syl31anc 1321 |
. . 3
⊢ (𝜑 → ((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}}))) |
119 | | vdgrval 26423 |
. . . 4
⊢ (((𝑉 ∈ V ∧ 𝐹 Fn 𝐵 ∧ 𝐵 ∈ 𝑌) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐹)‘𝑈) = ((#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}))) |
120 | 109, 12, 38, 114, 119 | syl31anc 1321 |
. . 3
⊢ (𝜑 → ((𝑉 VDeg 𝐹)‘𝑈) = ((#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}}))) |
121 | 118, 120 | oveq12d 6567 |
. 2
⊢ (𝜑 → (((𝑉 VDeg 𝐸)‘𝑈) +𝑒 ((𝑉 VDeg 𝐹)‘𝑈)) = (((#‘{𝑥 ∈ 𝐴 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐴 ∣ (𝐸‘𝑥) = {𝑈}})) +𝑒 ((#‘{𝑥 ∈ 𝐵 ∣ 𝑈 ∈ (𝐹‘𝑥)}) +𝑒 (#‘{𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) = {𝑈}})))) |
122 | 105, 116,
121 | 3eqtr4d 2654 |
1
⊢ (𝜑 → ((𝑉 VDeg (𝐸 ∪ 𝐹))‘𝑈) = (((𝑉 VDeg 𝐸)‘𝑈) +𝑒 ((𝑉 VDeg 𝐹)‘𝑈))) |