Metamath Proof Explorer

Theorem evlselvlem

Description: Lemma for evlselv . Used to re-index to and from bags of variables in I and bags of variables in the subsets J and I \ J . (Contributed by SN, 10-Mar-2025)

Ref Expression
Hypotheses evlselvlem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
evlselvlem.e ⊢ 𝐸 = { 𝑔 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑔 “ ℕ ) ∈ Fin }
evlselvlem.c ⊢ 𝐶 = { 𝑓 ∈ ( ℕ0 ↑m ( 𝐼 ∖ 𝐽 ) ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
evlselvlem.h ⊢ 𝐻 = ( 𝑐 ∈ 𝐶 , 𝑒 ∈ 𝐸 ↦ ( 𝑐 ∪ 𝑒 ) )
evlselvlem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
evlselvlem.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
Assertion evlselvlem ( 𝜑 → 𝐻 : ( 𝐶 × 𝐸 ) –1-1-onto→ 𝐷 )

Proof

Step Hyp Ref Expression
1 evlselvlem.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2 evlselvlem.e ⊢ 𝐸 = { 𝑔 ∈ ( ℕ0 ↑m 𝐽 ) ∣ ( ◡ 𝑔 “ ℕ ) ∈ Fin }
3 evlselvlem.c ⊢ 𝐶 = { 𝑓 ∈ ( ℕ0 ↑m ( 𝐼 ∖ 𝐽 ) ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
4 evlselvlem.h ⊢ 𝐻 = ( 𝑐 ∈ 𝐶 , 𝑒 ∈ 𝐸 ↦ ( 𝑐 ∪ 𝑒 ) )
5 evlselvlem.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 evlselvlem.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
7 3 psrbagf ⊢ ( 𝑐 ∈ 𝐶 → 𝑐 : ( 𝐼 ∖ 𝐽 ) ⟶ ℕ0 )
8 7 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 : ( 𝐼 ∖ 𝐽 ) ⟶ ℕ0 )
9 2 psrbagf ⊢ ( 𝑒 ∈ 𝐸 → 𝑒 : 𝐽 ⟶ ℕ0 )
10 9 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 : 𝐽 ⟶ ℕ0 )
11 disjdifr ⊢ ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅
12 11 a1i ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ )
13 8 10 12 fun2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) : ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) ⟶ ℕ0 )
14 undifr ⊢ ( 𝐽 ⊆ 𝐼 ↔ ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
15 6 14 sylib ⊢ ( 𝜑 → ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
17 16 feq2d ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) : ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) ⟶ ℕ0 ↔ ( 𝑐 ∪ 𝑒 ) : 𝐼 ⟶ ℕ0 ) )
18 13 17 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) : 𝐼 ⟶ ℕ0 )
19 unexg ⊢ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) → ( 𝑐 ∪ 𝑒 ) ∈ V )
20 19 adantl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) ∈ V )
21 0zd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 0 ∈ ℤ )
22 13 ffund ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → Fun ( 𝑐 ∪ 𝑒 ) )
23 3 psrbagfsupp ⊢ ( 𝑐 ∈ 𝐶 → 𝑐 finSupp 0 )
24 23 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 finSupp 0 )
25 2 psrbagfsupp ⊢ ( 𝑒 ∈ 𝐸 → 𝑒 finSupp 0 )
26 25 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 finSupp 0 )
27 24 26 fsuppun ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) supp 0 ) ∈ Fin )
28 20 21 22 27 isfsuppd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) finSupp 0 )
29 fcdmnn0fsuppg ⊢ ( ( ( 𝑐 ∪ 𝑒 ) ∈ V ∧ ( 𝑐 ∪ 𝑒 ) : ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) ⟶ ℕ0 ) → ( ( 𝑐 ∪ 𝑒 ) finSupp 0 ↔ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) )
30 20 13 29 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) finSupp 0 ↔ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) )
31 28 30 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin )
32 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝐼 ∈ 𝑉 )
33 1 psrbag ⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝑐 ∪ 𝑒 ) ∈ 𝐷 ↔ ( ( 𝑐 ∪ 𝑒 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) ) )
34 32 33 syl ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) ∈ 𝐷 ↔ ( ( 𝑐 ∪ 𝑒 ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑐 ∪ 𝑒 ) “ ℕ ) ∈ Fin ) ) )
35 18 31 34 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 ∪ 𝑒 ) ∈ 𝐷 )
36 5 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
37 difssd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝐼 ∖ 𝐽 ) ⊆ 𝐼 )
38 simpr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 ∈ 𝐷 )
39 1 3 36 37 38 psrbagres ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∈ 𝐶 )
40 6 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝐽 ⊆ 𝐼 )
41 1 2 36 40 38 psrbagres ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( 𝑑 ↾ 𝐽 ) ∈ 𝐸 )
42 1 psrbagf ⊢ ( 𝑑 ∈ 𝐷 → 𝑑 : 𝐼 ⟶ ℕ0 )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 : 𝐼 ⟶ ℕ0 )
44 43 freld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → Rel 𝑑 )
45 43 fdmd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → dom 𝑑 = 𝐼 )
46 40 14 sylib ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) = 𝐼 )
47 45 46 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → dom 𝑑 = ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) )
48 11 a1i ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ )
49 reldisjun ⊢ ( ( Rel 𝑑 ∧ dom 𝑑 = ( ( 𝐼 ∖ 𝐽 ) ∪ 𝐽 ) ∧ ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ) → 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
50 44 47 48 49 syl3anc ⊢ ( ( 𝜑 ∧ 𝑑 ∈ 𝐷 ) → 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
51 50 adantrl ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
52 uneq12 ⊢ ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) → ( 𝑐 ∪ 𝑒 ) = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) )
53 52 eqeq2d ⊢ ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) → ( 𝑑 = ( 𝑐 ∪ 𝑒 ) ↔ 𝑑 = ( ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∪ ( 𝑑 ↾ 𝐽 ) ) ) )
54 51 53 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) → 𝑑 = ( 𝑐 ∪ 𝑒 ) ) )
55 8 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 Fn ( 𝐼 ∖ 𝐽 ) )
56 10 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 Fn 𝐽 )
57 fnunres1 ⊢ ( ( 𝑐 Fn ( 𝐼 ∖ 𝐽 ) ∧ 𝑒 Fn 𝐽 ∧ ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ) → ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) = 𝑐 )
58 55 56 12 57 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) = 𝑐 )
59 58 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) )
60 fnunres2 ⊢ ( ( 𝑐 Fn ( 𝐼 ∖ 𝐽 ) ∧ 𝑒 Fn 𝐽 ∧ ( ( 𝐼 ∖ 𝐽 ) ∩ 𝐽 ) = ∅ ) → ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) = 𝑒 )
61 55 56 12 60 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) = 𝑒 )
62 61 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) )
63 59 62 jca ⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ) → ( 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) )
64 63 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) )
65 reseq1 ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) )
66 65 eqeq2d ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ↔ 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ) )
67 reseq1 ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑑 ↾ 𝐽 ) = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) )
68 67 eqeq2d ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑒 = ( 𝑑 ↾ 𝐽 ) ↔ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) )
69 66 68 anbi12d ⊢ ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) ↔ ( 𝑐 = ( ( 𝑐 ∪ 𝑒 ) ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( ( 𝑐 ∪ 𝑒 ) ↾ 𝐽 ) ) ) )
70 64 69 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( 𝑑 = ( 𝑐 ∪ 𝑒 ) → ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) ) )
71 54 70 impbid ⊢ ( ( 𝜑 ∧ ( ( 𝑐 ∈ 𝐶 ∧ 𝑒 ∈ 𝐸 ) ∧ 𝑑 ∈ 𝐷 ) ) → ( ( 𝑐 = ( 𝑑 ↾ ( 𝐼 ∖ 𝐽 ) ) ∧ 𝑒 = ( 𝑑 ↾ 𝐽 ) ) ↔ 𝑑 = ( 𝑐 ∪ 𝑒 ) ) )
72 4 35 39 41 71 f1o2d2 ⊢ ( 𝜑 → 𝐻 : ( 𝐶 × 𝐸 ) –1-1-onto→ 𝐷 )