Step |
Hyp |
Ref |
Expression |
1 |
|
fsuppunbi.u |
⊢ ( 𝜑 → Fun ( 𝐹 ∪ 𝐺 ) ) |
2 |
|
relfsupp |
⊢ Rel finSupp |
3 |
2
|
brrelex12i |
⊢ ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) ) |
4 |
|
unexb |
⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ↔ ( 𝐹 ∪ 𝐺 ) ∈ V ) |
5 |
|
simpr |
⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) |
6 |
5
|
adantr |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) |
7 |
|
simprlr |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → 𝐺 ∈ V ) |
8 |
7
|
suppun |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐹 supp 𝑍 ) ⊆ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ) |
9 |
6 8
|
ssfid |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐹 supp 𝑍 ) ∈ Fin ) |
10 |
|
fununfun |
⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → ( Fun 𝐹 ∧ Fun 𝐺 ) ) |
11 |
10
|
simpld |
⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → Fun 𝐹 ) |
12 |
11
|
adantr |
⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → Fun 𝐹 ) |
13 |
12
|
adantr |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → Fun 𝐹 ) |
14 |
|
simprll |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → 𝐹 ∈ V ) |
15 |
|
simpr |
⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) → 𝑍 ∈ V ) |
16 |
15
|
adantl |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → 𝑍 ∈ V ) |
17 |
|
funisfsupp |
⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) ) |
18 |
13 14 16 17
|
syl3anc |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) ) |
19 |
9 18
|
mpbird |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → 𝐹 finSupp 𝑍 ) |
20 |
|
uncom |
⊢ ( 𝐹 ∪ 𝐺 ) = ( 𝐺 ∪ 𝐹 ) |
21 |
20
|
oveq1i |
⊢ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) = ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) |
22 |
21
|
eleq1i |
⊢ ( ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ↔ ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) ∈ Fin ) |
23 |
22
|
biimpi |
⊢ ( ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin → ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) ∈ Fin ) |
24 |
23
|
adantl |
⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) ∈ Fin ) |
25 |
24
|
adantr |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) ∈ Fin ) |
26 |
14
|
suppun |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐺 supp 𝑍 ) ⊆ ( ( 𝐺 ∪ 𝐹 ) supp 𝑍 ) ) |
27 |
25 26
|
ssfid |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐺 supp 𝑍 ) ∈ Fin ) |
28 |
10
|
simprd |
⊢ ( Fun ( 𝐹 ∪ 𝐺 ) → Fun 𝐺 ) |
29 |
28
|
adantr |
⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → Fun 𝐺 ) |
30 |
29
|
adantr |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → Fun 𝐺 ) |
31 |
|
funisfsupp |
⊢ ( ( Fun 𝐺 ∧ 𝐺 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) ) |
32 |
30 7 16 31
|
syl3anc |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) ) |
33 |
27 32
|
mpbird |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → 𝐺 finSupp 𝑍 ) |
34 |
19 33
|
jca |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) |
35 |
34
|
a1d |
⊢ ( ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ∧ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) ) → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) |
36 |
35
|
ex |
⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) → ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) ) |
37 |
|
fsuppimp |
⊢ ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ) |
38 |
36 37
|
syl11 |
⊢ ( ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) ) |
39 |
4 38
|
sylanbr |
⊢ ( ( ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) ) |
40 |
3 39
|
mpcom |
⊢ ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝜑 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) |
41 |
40
|
com12 |
⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 → ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) |
42 |
|
simpl |
⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → 𝐹 finSupp 𝑍 ) |
43 |
|
simpr |
⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → 𝐺 finSupp 𝑍 ) |
44 |
42 43
|
fsuppun |
⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) |
45 |
44
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) |
46 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → Fun ( 𝐹 ∪ 𝐺 ) ) |
47 |
2
|
brrelex1i |
⊢ ( 𝐹 finSupp 𝑍 → 𝐹 ∈ V ) |
48 |
2
|
brrelex1i |
⊢ ( 𝐺 finSupp 𝑍 → 𝐺 ∈ V ) |
49 |
|
unexg |
⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 𝐹 ∪ 𝐺 ) ∈ V ) |
50 |
47 48 49
|
syl2an |
⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( 𝐹 ∪ 𝐺 ) ∈ V ) |
51 |
50
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( 𝐹 ∪ 𝐺 ) ∈ V ) |
52 |
2
|
brrelex2i |
⊢ ( 𝐹 finSupp 𝑍 → 𝑍 ∈ V ) |
53 |
52
|
adantr |
⊢ ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → 𝑍 ∈ V ) |
54 |
53
|
adantl |
⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → 𝑍 ∈ V ) |
55 |
|
funisfsupp |
⊢ ( ( Fun ( 𝐹 ∪ 𝐺 ) ∧ ( 𝐹 ∪ 𝐺 ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ) |
56 |
46 51 54 55
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ↔ ( ( 𝐹 ∪ 𝐺 ) supp 𝑍 ) ∈ Fin ) ) |
57 |
45 56
|
mpbird |
⊢ ( ( 𝜑 ∧ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) → ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ) |
58 |
57
|
ex |
⊢ ( 𝜑 → ( ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) → ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ) ) |
59 |
41 58
|
impbid |
⊢ ( 𝜑 → ( ( 𝐹 ∪ 𝐺 ) finSupp 𝑍 ↔ ( 𝐹 finSupp 𝑍 ∧ 𝐺 finSupp 𝑍 ) ) ) |